CVC4, the smt solver, 2011. ,
Interactive Theorem Proving and Program Development . Coq'Art: The Calculus of Inductive Constructions, 2004. ,
URL : https://hal.archives-ouvertes.fr/hal-00344237
The alt-ergo automated theorem prover, 2008. ,
Why3: Shepherd your herd of provers, Boogie 2011: First International Workshop on Intermediate Verification Languages, pp.53-64, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00790310
The coq 8.5 standard library, 2015. ,
Introduction to Algorithms, 2001. ,
Z3, an efficient smt solver. Microsoft Research, 2008. ,
Informatique et sciences du numérique-Spécialité ISN en terminale S. Eyrolles, 2012. ,
The why3 gallery of verified programs, 2015. ,
Why3 ??? Where Programs Meet Provers, Proceedings of the 22nd European Symposium on Programming, pp.125-128, 2013. ,
DOI : 10.1007/978-3-642-37036-6_8
Finite graphs in mathematical components Available at http://ssr.msr-inria.inria.fr/ ? jenkins/current/Ssreflect.fingraph.html, The full library is available at http://www.msr-inria, 2012. ,
A Modular Formalisation of Finite Group Theory, Theorem Proving in Higher-Order Logics (TPHOLS'07), pp.86-101, 2007. ,
DOI : 10.1007/978-3-540-74591-4_8
URL : https://hal.archives-ouvertes.fr/inria-00139131
A Small Scale Reflection Extension for the Coq system, 2008. ,
URL : https://hal.archives-ouvertes.fr/inria-00258384
A Framework for Verifying Depth-First Search Algorithms, Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP '15, pp.137-146, 2015. ,
DOI : 10.1145/2676724.2693165
Formal verification of a realistic compiler, Communications of the ACM, vol.52, issue.7, 2009. ,
DOI : 10.1145/1538788.1538814
URL : https://hal.archives-ouvertes.fr/inria-00415861
Essays for the Luca Cardelli Fest, chapter Simple proofs of simple programs in Why3, 2014. ,
Formal Analysis of the Operational Concept for the Small Aircraft Transportation System, Rigorous Engineering of Fault- Tolerant Systems, pp.306-325, 2006. ,
DOI : 10.1007/11916246_16
Depth-first search and strong connectivity in Coq, Journées Francophones des Langages Applicatifs, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01096354
System Description: E??1.8, Proc. of the 19th LPAR, 2013. ,
DOI : 10.1007/978-3-642-45221-5_49
Binary heaps formally verified in Why3, Research Report, vol.7780, 2011. ,
URL : https://hal.archives-ouvertes.fr/inria-00636083
SPASS Version 3.5, 22nd International Conference on Automated Deduction number 5663 in LNCS, pp.140-145, 2009. ,
DOI : 10.1007/978-3-540-73595-3_38