A. W. Appel, Verified Functional Algorithms. www.cs.princeton, 2016.

F. Bobot, J. Filliâtre, C. Marché, G. Melquiond, and A. Paskevich, The Why3 platform, version 0.86.1. LRI, CNRS & Univ, 2015.

A. Charguéraud, Program verification through characteristic formulae, Proceeding of the 15th ACM SIGPLAN international conference on Functional programming (ICFP), pp.321-332, 2010.

A. Charguéraud, 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

A. Charguéraud and F. Pottier, 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

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.

J. Filliâtre, L. Gondelman, and A. Paskevich, The spirit of ghost code. Formal Methods in System Design, 2016.

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, 2012.

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

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

F. Mehta and T. Nipkow, Proving pointer programs in higher-order logic, CADE, 2003.

C. M. Poskitt and D. Plump, Hoare logic for graph programs, VSTTE, 2010.

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

M. Sharir, 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

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

I. Wengener, 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