Y. Bertot and P. Castéran, Interactive Theorem Proving and Program Development. Coq'Art : The Calculus of Inductive Constructions, 2004.
DOI : 10.1007/978-3-662-07964-5
URL : https://hal.archives-ouvertes.fr/hal-00344237

F. Bobot, S. Conchon, E. Contejean, M. Iguernelala, S. Lescuyer et al., The alt-ergo automated theorem prover, 2008.

F. Bobot, J. Filliâtre, C. Marché, and A. Paskevich, 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

C. Development and T. , The coq 8.5 standard library, 2015.

T. H. Cormen, C. Stein, R. L. Rivest, and C. E. Leiserson, Introduction to Algorithms, 2001.

L. De-moura and N. Björner, Z3, an efficient smt solver. Microsoft Research, 2008.

G. Dowek, Informatique et sciences du numérique-Spécialité ISN en terminale S. Eyrolles, 2012.

J. Filliâtre, The why3 gallery of verified programs, 2015.

J. Filliâtre and A. Paskevich, 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

G. Gonthier, 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.

G. Gonthier, A. Mahboubi, L. Rideau, E. Tassi, and L. Théry, 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

G. Gonthier, A. Mahboubi, and E. Tassi, A Small Scale Reflection Extension for the Coq system, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00258384

P. Lammich and R. Neumann, 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

X. Leroy, 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

J. Lévy, Essays for the Luca Cardelli Fest, chapter Simple proofs of simple programs in Why3, 2014.

F. Pottier, Depth-first search and strong connectivity in Coq, Journées Francophones des Langages Applicatifs, 2015.
URL : https://hal.archives-ouvertes.fr/hal-01096354

S. Schulz, System Description: E??1.8, Proc. of the 19th LPAR, 2013.
DOI : 10.1007/978-3-642-45221-5_49

A. Tafat and C. Marché, Binary heaps formally verified in Why3, Research Report, vol.7780, 2011.
URL : https://hal.archives-ouvertes.fr/inria-00636083

R. Tarjan, Depth-First Search and Linear Graph Algorithms, SIAM Journal on Computing, vol.1, issue.2, pp.146-160, 1972.
DOI : 10.1137/0201010
URL : http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.327.8418

L. Théry, Formally-proven Kosaraju's algorithm

C. Weidenbach, D. Dimova, A. Fietzke, R. Kumar, M. Suda et al., 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