J. Alpuim and W. Swierstra, Embedding the refinement calculus in Coq, Sci. Comput. Program, vol.164, pp.37-48, 2018.

G. Barthe, J. Forest, D. Pichardie, and V. Rusu, Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant, Functional and LOgic Programming Systems (FLOPS'06), vol.3945, pp.114-129, 2006.
URL : https://hal.archives-ouvertes.fr/inria-00564237

S. Jasmin-christian-blanchette, L. C. Böhme, and . Paulson, Extending Sledgehammer with SMT Solvers, J. Automated Reasoning, vol.51, issue.1, pp.109-128, 2013.

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

A. Bove, A. Krauss, and M. Sozeau, Partiality and recursion in interactive theorem provers -an overview, Mathematical Structures in Computer Science, vol.26, issue.1, pp.38-88, 2016.
URL : https://hal.archives-ouvertes.fr/hal-00691459

A. Charguéraud, Characteristic formulae for the verification of imperative programs, Proc. 16th ACM SIGPLAN Intl. Conf. Functional Programming, pp.418-430, 2011.

A. Charguéraud, Higher-order Representation Predicates in Separation Logic, Proc. 5th ACM SIGPLAN Conf. Certified Programs and Proofs, pp.3-14, 2016.

R. Chen and J. Lévy, A Semi-automatic Proof of Strong connectivity, LNCS, vol.10712, pp.49-65, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01632947

R. Chen and J. Lévy, Full scripts of Tarjan SCC Why3 proof, Iscas and Inria, 2017. jeanjacqueslevy.net/why3, vol.13, p.18

, Formal Proofs of Tarjan's SCC Algorithm

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

?. Czajka and C. Kaliszyk, Hammer for Coq: Automation for Dependent Type Theory, J. Autom. Reasoning, pp.423-453, 2018.

C. Doczkal, G. Combette, and D. Pous, A Formal Proof of the MinorExclusion Property for Treewidth-Two Graphs, ITP 2018, vol.10895, pp.178-195, 2018.
URL : https://hal.archives-ouvertes.fr/hal-01703922

B. Ekici, A. Mebsout, C. Tinelli, C. Keller, G. Katz et al., SMTCoq: A plug-in for integrating SMT solvers into Coq, CAV, vol.10427, pp.126-133, 2017.
URL : https://hal.archives-ouvertes.fr/hal-01669345

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

G. Gonthier and A. Mahboubi, An introduction to small scale reflection in Coq, J. Formalized Reasoning, vol.3, issue.2, pp.95-152, 2010.
URL : https://hal.archives-ouvertes.fr/inria-00515548

A. Hobor and J. Villard, The Ramifications of Sharing in Data Structures, Proc. 40th Ann. ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, POPL '13, pp.523-536, 2013.

P. Lammich, Refinement for Monadic Programs. Archive of Formal Proofs, 2012.

P. Lammich, Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm, ITP 2015, vol.8558, pp.325-340, 2014.

P. Lammich, Refinement to Imperative/HOL, J. Automated Reasoning, 2019.

P. Lammich and R. Neumann, A Framework for Verifying Depth-First Search Algorithms, Proc. 4th ACM SIGPLAN Conf. Certified Programs and Proofs, CPP '15, pp.137-146, 2015.

A. Mahboubi and E. Tassi, Mathematical Components. Available, 2016.

F. Mehta and T. Nipkow, Proving Pointer Programs in Higher-Order Logic, CADE, 2003.

S. Merz, Formalization of Tarjan's Algorithm in Isabelle, 2018.

T. Nipkow, L. Paulson, and M. Wenzel, Isabelle/HOL. A Proof Assistant for Higher-Order Logic. Number 2283 in Lecture Notes in Computer Science, 2002.

L. Noschinski, A Graph Library for Isabelle, Mathematics in Computer Science, vol.9, issue.1, pp.23-39, 2015.

L. C. Paulson, Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science, vol.828, 1994.

M. Christopher, D. Poskitt, and . Plump, Hoare-Style Verification of Graph Programs, Fundamenta Informaticae, vol.118, issue.1-2, pp.135-175, 2012.

F. Pottier, Depth-First Search and Strong Connectivity in Coq, Journées Francophones des Langages Applicatifs (JFLA 2015), 2015.
URL : https://hal.archives-ouvertes.fr/hal-01096354

A. Raad, A. Hobor, J. Villard, and P. Gardner, Verifying Concurrent Graph Algorithms, APLAS 2016, vol.10017, pp.314-334, 2016.

I. Sergey, A. Nanevski, and A. Banerjee, Mechanized Verification of Finegrained Concurrent Programs, Proc. 36th ACM SIGPLAN Conf. Programming Language Design and Implementation, PLDI '15, pp.77-87, 2015.

R. Tarjan, Depth first search and linear graph algorithms, SIAM Journal on Computing, 1972.

L. Théry, Formally-proven Kosaraju's algorithm, 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.

M. Wenzel, Isar -A Generic Interpretative Approach to Readable Formal Proof Documents, TPHOLS'99, vol.1690, pp.167-184, 1999.

F. Wiedijk, The Seventeen Provers of the World, LNCS. Springer, vol.3600, 2006.