Verified Functional Algorithms. www.cs.princeton, 2016. ,
The Why3 platform, version 0.86.1. LRI, CNRS & Univ, 2015. ,
Program verification through characteristic formulae, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming (ICFP), pp.321-332, 2010. ,
Higher-order representation predicates in separation logic, Proceedings of the 5th ACM SIGPLAN Conference on Certified Programs and Proofs, CPP 2016, pp.3-14, 2016. ,
DOI : 10.1145/2854065.2854068
Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation, p.2015 ,
DOI : 10.1007/978-3-319-22102-1_9
The coq 8.5 standard library, 2015. ,
Introduction to Algorithms, 2001. ,
The spirit of ghost code. Formal Methods in System Design, 2016. ,
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, 2012. ,
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
Essays for the Luca Cardelli Fest, chapter Simple proofs of simple programs in Why3, 2014. ,
Proving pointer programs in higher-order logic, CADE, 2003. ,
Hoare logic for graph programs, VSTTE, 2010. ,
Depth-first search and strong connectivity in Coq, Journées Francophones des Langages Applicatifs, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01096354
A strong-connectivity algorithm and its applications in data flow analysis, Computers & Mathematics with Applications, vol.7, issue.1, pp.67-72, 1981. ,
DOI : 10.1016/0898-1221(81)90008-0
Formally-proven Kosaraju's algorithm. Inria report, 2015. ,
A simplified correctness proof for a well-known algorithm computing strongly connected components, Information Processing Letters, vol.83, issue.1, pp.17-19, 2002. ,
DOI : 10.1016/S0020-0190(01)00306-4