A Machine-checked Proof of the Average-case Complexity of Quicksort in Coq

Autor: Weegen, E.E. van der, McKinna, J.H., Berardi, Stefano, Liquori, Ugo de

Publikováno v: Berardi, Stefano; Liquori, Ugo de (ed.), Types for Proofs International Conference, TYPES 2008 Torino, Italy, 256-271. Berlin / Heidelberg : Springer
STARTPAGE=256;ENDPAGE=271;ISSN=0302-9743;TITLE=Berardi, Stefano; Liquori, Ugo de (ed.), Types for Proofs International Conference, TYPES 2008 Torino, Italy
Berardi, Stefano; Liquori, Ugo de (ed.), Types for Proofs International Conference, TYPES 2008 Torino, Italy, pp. 256-271

Item does not contain fulltext Types for Proofs International Conference, TYPES 2008 Torino, Italy, 26 maart 2008

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::4a6066737aa728f33d5188cfeec638bc
https://hdl.handle.net/2066/76114

Automated machine-checked hybrid system safety proofs

Autor: Kaufmann, M., Paulson, L., Geuvers, H., Koprowski, A., Synek, D., Weegen, E.E. van der

Publikováno v: Interactive Theorem Proving ISBN: 9783642140518
ITP
Lecture Notes in Computer Science ; 6172, 259-274. Berlin / Heidelberg : Springer
STARTPAGE=259;ENDPAGE=274;TITLE=Lecture Notes in Computer Science ; 6172
Interactive Theorem Proving, pp. 259-274
Interactive Theorem Proving (First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings), 259-274
STARTPAGE=259;ENDPAGE=274;TITLE=Interactive Theorem Proving (First International Conference, ITP 2010, Edinburgh, UK, July 11-14, 2010. Proceedings)

We have developed a hybrid system safety prover, implemented in Coq using the abstraction method introduced by [2]. The development includes: a formalisation of the structure of hybrid systems; a framework for the construction of an abstract system (

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::52d814d1349894a149aeb0fe445c1b60
https://research.tue.nl/en/publications/f2446479-a072-4c80-949c-4e61a2a12b79