A. V. Aho, J. E. Hopcroft, and J. D. Ullman, The Design and Analysis of Computer Algorithms, 1974.

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

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

F. Bobot, J. C. Filliâtre, C. Marché, G. Melquiond, and A. Paskevich, Preserving User Proofs across Specification Changes, Fifth Working Conference on Verified Software: Theories, Tools and Experiments, pp.191-201, 2013.
DOI : 10.1007/978-3-642-54108-7_10
URL : https://hal.archives-ouvertes.fr/hal-00875395

F. Bobot, J. C. Filliâtre, C. Marché, and A. Paskevich, Let???s verify this with Why3, International Journal on Software Tools for Technology Transfer, vol.7, issue.5, pp.709-727, 2015.
DOI : 10.1007/978-3-642-02959-2_10

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.1016/j.entcs.2008.10.022

A. Charguéraud and F. Pottier, Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation, Proceedings of the 6th International Conference on Interactive Theorem Proving (ITP), 2015.
DOI : 10.1007/978-3-319-22102-1_9

R. Chen and J. J. Lévy, Full script of Tarjan SCC Why3 proof, Iscas and Inria, 2017.

R. Chen and J. J. Lévy, Une preuve formelle de l'algorithme de Tarjan-1972 pour trouver les composantes fortement connexes dans un graphe, p.JFLA, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01422215

M. Clochard, Preuves taillées en biseau In: vingthuitì emes Journées Francophones des Langages Applicatifs (JFLA), 2017.

C. Cohen and L. Théry, Full script of Tarjan SCC Coq/ssreflect proof, Tech. rep. Inria, 2017.

J. C. 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, A. Mahboubi, and E. Tassi, A Small Scale Reflection Extension for the Coq system, INRIA, 2008.
URL : https://hal.archives-ouvertes.fr/inria-00258384

G. Gonthier, Finite graphs in mathematical components (2012), ssr. msr-inria.inria.fr/ ~ jenkins/current/Ssreflect.fingraph.html, The full library is available at www.msr-inria

A. Hobor and J. Villard, The ramifications of sharing in data structures, Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp.523-536, 2013.

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.1137/0201010

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

F. Mehta and T. Nipkow, Proving pointer programs in higher-order logic, p.CADE, 2003.
DOI : 10.1016/j.ic.2004.10.007
URL : https://doi.org/10.1016/j.ic.2004.10.007

C. M. Poskitt and D. Plump, Hoare logic for graph programs, p.VSTTE, 2010.
DOI : 10.1007/978-3-642-15928-2_10
URL : http://www.cs.york.ac.uk/plasma/publications/pdf/PoskittPlump.ICGT.10.pdf

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

A. Raad, A. Hobor, J. Villard, and P. Gardner, Verifying Concurrent Graph Algorithms, pp.314-334978, 2016.
DOI : 10.1145/2500365.2500600

I. Sergey, A. Nanevski, and A. Banerjee, Mechanized verification of fine-grained concurrent programs, Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, pp.77-87, 2015.
DOI : 10.1145/2737924.2737964
URL : http://ilyasergey.net/papers/fcsl-pldi15-draft.pdf

R. Tarjan, Depth first search and linear graph algorithms, SIAM Journal on Computing, 1972.
DOI : 10.1137/0201010

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

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