Embedding the refinement calculus in Coq, Sci. Comput. Program, vol.164, pp.37-48, 2018. ,
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
Extending Sledgehammer with SMT Solvers, J. Automated Reasoning, vol.51, issue.1, pp.109-128, 2013. ,
The Why3 platform, version 0.86.1. LRI, 2015. ,
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
Characteristic formulae for the verification of imperative programs, Proc. 16th ACM SIGPLAN Intl. Conf. Functional Programming, pp.418-430, 2011. ,
Higher-order Representation Predicates in Separation Logic, Proc. 5th ACM SIGPLAN Conf. Certified Programs and Proofs, pp.3-14, 2016. ,
A Semi-automatic Proof of Strong connectivity, LNCS, vol.10712, pp.49-65, 2017. ,
URL : https://hal.archives-ouvertes.fr/hal-01632947
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
Full script of Tarjan SCC Coq/ssreflect proof, 2017. ,
Hammer for Coq: Automation for Dependent Type Theory, J. Autom. Reasoning, pp.423-453, 2018. ,
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
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
The Why3 gallery of verified programs, CNRS, 2015. ,
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
The Ramifications of Sharing in Data Structures, Proc. 40th Ann. ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, POPL '13, pp.523-536, 2013. ,
Refinement for Monadic Programs. Archive of Formal Proofs, 2012. ,
Verified Efficient Implementation of Gabow's Strongly Connected Component Algorithm, ITP 2015, vol.8558, pp.325-340, 2014. ,
Refinement to Imperative/HOL, J. Automated Reasoning, 2019. ,
A Framework for Verifying Depth-First Search Algorithms, Proc. 4th ACM SIGPLAN Conf. Certified Programs and Proofs, CPP '15, pp.137-146, 2015. ,
, Mathematical Components. Available, 2016.
Proving Pointer Programs in Higher-Order Logic, CADE, 2003. ,
Formalization of Tarjan's Algorithm in Isabelle, 2018. ,
Isabelle/HOL. A Proof Assistant for Higher-Order Logic. Number 2283 in Lecture Notes in Computer Science, 2002. ,
A Graph Library for Isabelle, Mathematics in Computer Science, vol.9, issue.1, pp.23-39, 2015. ,
Isabelle: A Generic Theorem Prover, Lecture Notes in Computer Science, vol.828, 1994. ,
Hoare-Style Verification of Graph Programs, Fundamenta Informaticae, vol.118, issue.1-2, pp.135-175, 2012. ,
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
Verifying Concurrent Graph Algorithms, APLAS 2016, vol.10017, pp.314-334, 2016. ,
Mechanized Verification of Finegrained Concurrent Programs, Proc. 36th ACM SIGPLAN Conf. Programming Language Design and Implementation, PLDI '15, pp.77-87, 2015. ,
Depth first search and linear graph algorithms, SIAM Journal on Computing, 1972. ,
Formally-proven Kosaraju's algorithm, 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. ,
Isar -A Generic Interpretative Approach to Readable Formal Proof Documents, TPHOLS'99, vol.1690, pp.167-184, 1999. ,
The Seventeen Provers of the World, LNCS. Springer, vol.3600, 2006. ,