Document Open Access Logo

Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle

Authors Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, Laurent Théry

PDF
Thumbnail PDF

File

LIPIcs.ITP.2019.13.pdf
  • Filesize: 0.55 MB
  • 19 pages

Document Identifiers

Author Details

Ran Chen
  • Institute of Software of the Chinese Academy of Sciences, Beijing, China
Cyril Cohen
  • Université Côte d'Azur, Inria, Sophia Antipolis, France
Jean-Jacques Lévy
  • Irif & Inria, Paris, France
Stephan Merz
  • Université de Lorraine, CNRS, Inria, LORIA, Nancy, France
Laurent Théry
  • Université Côte d'Azur, Inria, Sophia Antipolis, France

Cite As Get BibTex

Ran Chen, Cyril Cohen, Jean-Jacques Lévy, Stephan Merz, and Laurent Théry. Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle. In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019) https://doi.org/10.4230/LIPIcs.ITP.2019.13

Abstract

Comparing provers on a formalization of the same problem is always a valuable exercise. In this paper, we present the formal proof of correctness of a non-trivial algorithm from graph theory that was carried out in three proof assistants: Why3, Coq, and Isabelle.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Formal software verification
Keywords
  • Mathematical logic
  • Formal proof
  • Graph algorithm
  • Program verification

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. João Alpuim and Wouter Swierstra. Embedding the refinement calculus in Coq. Sci. Comput. Program., 164:37-48, 2018. Google Scholar
  2. G. Barthe, J. Forest, D. Pichardie, and V. Rusu. Defining and reasoning about recursive functions: a practical tool for the Coq proof assistant. In Functional and LOgic Programming Systems (FLOPS'06), volume 3945 of LNCS, pages 114-129, Fuji Susono, Japan, April 2006. Google Scholar
  3. Jasmin Christian Blanchette, Sascha Böhme, and Lawrence C. Paulson. Extending Sledgehammer with SMT Solvers. J. Automated Reasoning, 51(1):109-128, 2013. Google Scholar
  4. François Bobot, Jean-Christophe Filliâtre, Claude Marché, Guillaume Melquiond, and Andrei Paskevich. The Why3 platform, version 0.86.1. LRI, CNRS & Univ. Paris-Sud & INRIA Saclay, version 0.86.1 edition, May 2015. Available at https://why3.lri.fr/download/manual-0.86.1.pdf.
  5. Ana Bove, Alexander Krauss, and Matthieu Sozeau. Partiality and recursion in interactive theorem provers - an overview. Mathematical Structures in Computer Science, 26(1):38-88, 2016. Google Scholar
  6. Arthur Charguéraud. Characteristic formulae for the verification of imperative programs. In Proc. 16th ACM SIGPLAN Intl. Conf. Functional Programming, pages 418-430, Tokyo, Japan, 2011. ACM. Google Scholar
  7. Arthur Charguéraud. Higher-order Representation Predicates in Separation Logic. In Proc. 5th ACM SIGPLAN Conf. Certified Programs and Proofs, CPP 2016, pages 3-14, New York, NY, USA, 2016. ACM. Google Scholar
  8. Ran Chen and Jean-Jacques Lévy. A Semi-automatic Proof of Strong connectivity. In VSTTE 2017, volume 10712 of LNCS, pages 49-65. Springer, 2017. Google Scholar
  9. Ran Chen and Jean-Jacques Lévy. Full scripts of Tarjan SCC Why3 proof. Technical report, Iscas and Inria, 2017. https://jeanjacqueslevy.net/why3.
  10. Cyril Cohen and Laurent Théry. Full script of Tarjan SCC Coq/ssreflect proof, 2017. Available at https://www-sop.inria.fr/marelle/Tarjan/.
  11. Łukasz Czajka and Cezary Kaliszyk. Hammer for Coq: Automation for Dependent Type Theory. J. Autom. Reasoning, 61(1-4):423-453, 2018. Google Scholar
  12. Christian Doczkal, Guillaume Combette, and Damien Pous. A Formal Proof of the Minor-Exclusion Property for Treewidth-Two Graphs. In ITP 2018, volume 10895 of LNCS, pages 178-195. Springer, 2018. Google Scholar
  13. Burak Ekici, Alain Mebsout, Cesare Tinelli, Chantal Keller, Guy Katz, Andrew Reynolds, and Clark W. Barrett. SMTCoq: A plug-in for integrating SMT solvers into Coq. In CAV (2), volume 10427 of LNCS, pages 126-133. Springer, 2017. Google Scholar
  14. Jean-Christophe Filliâtre et al. The Why3 gallery of verified programs. Technical report, CNRS, Inria, U. Paris-Sud, 2015. https://toccata.lri.fr/gallery/why3.en.html.
  15. Georges Gonthier and Assia Mahboubi. An introduction to small scale reflection in Coq. J. Formalized Reasoning, 3(2):95-152, 2010. Google Scholar
  16. Aquinas Hobor and Jules Villard. The Ramifications of Sharing in Data Structures. In Proc. 40th Ann. ACM SIGPLAN-SIGACT Symp. Principles of Programming Languages, POPL '13, pages 523-536, New York, NY, USA, 2013. ACM. Google Scholar
  17. Peter Lammich. Refinement for Monadic Programs. Archive of Formal Proofs, 2012. URL: https://www.isa-afp.org/entries/Refine_Monadic.shtml.
  18. Peter Lammich. Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm. In ITP 2015, volume 8558 of LNCS, pages 325-340, Vienna, Austria, 2014. Springer. Google Scholar
  19. Peter Lammich. Refinement to Imperative/HOL. J. Automated Reasoning, 2019. Google Scholar
  20. Peter Lammich and René Neumann. A Framework for Verifying Depth-First Search Algorithms. In Proc. 4th ACM SIGPLAN Conf. Certified Programs and Proofs, CPP '15, pages 137-146, New York, NY, USA, 2015. ACM. Google Scholar
  21. Assia Mahboubi and Enrico Tassi. Mathematical Components. Available at: https://math-comp.github.io/mcb/, 2016.
  22. Farhad Mehta and Tobias Nipkow. Proving Pointer Programs in Higher-Order Logic. In CADE, 2003. Google Scholar
  23. Stephan Merz. Formalization of Tarjan’s Algorithm in Isabelle, 2018. Available at https://members.loria.fr/SMerz/projects/tarjan/index.html.
  24. Tobias Nipkow, Lawrence Paulson, and Markus Wenzel. Isabelle/HOL. A Proof Assistant for Higher-Order Logic. Number 2283 in Lecture Notes in Computer Science. Springer Verlag, 2002. Google Scholar
  25. Lars Noschinski. A Graph Library for Isabelle. Mathematics in Computer Science, 9(1):23-39, 2015. Google Scholar
  26. Lawrence C. Paulson. Isabelle: A Generic Theorem Prover, volume 828 of Lecture Notes in Computer Science. Springer Verlag, 1994. Google Scholar
  27. Christopher M. Poskitt and Detlef Plump. Hoare-Style Verification of Graph Programs. Fundamenta Informaticae, 118(1-2):135-175, 2012. Google Scholar
  28. François Pottier. Depth-First Search and Strong Connectivity in Coq. In Journées Francophones des Langages Applicatifs (JFLA 2015), January 2015. Google Scholar
  29. Azalea Raad, Aquinas Hobor, Jules Villard, and Philippa Gardner. Verifying Concurrent Graph Algorithms. In APLAS 2016, volume 10017 of LNCS, pages 314-334, Hanoi, Vietnam, 2016. Springer. Google Scholar
  30. Ilya Sergey, Aleksandar Nanevski, and Anindya Banerjee. Mechanized Verification of Fine-grained Concurrent Programs. In Proc. 36th ACM SIGPLAN Conf. Programming Language Design and Implementation, PLDI '15, pages 77-87, New York, NY, USA, 2015. ACM. Google Scholar
  31. Robert Tarjan. Depth first search and linear graph algorithms. SIAM Journal on Computing, 1972. Google Scholar
  32. Laurent Théry. Formally-proven Kosaraju’s algorithm. Inria report, Hal-01095533, 2015. Google Scholar
  33. Ingo Wengener. A Simplified Correctness Proof for a Well-Known Algorithm Computing Strongly Connected Components. Information Processing Letters, 83(1):17-19, 2002. Google Scholar
  34. Markus Wenzel. Isar - A Generic Interpretative Approach to Readable Formal Proof Documents. In TPHOLS'99, volume 1690 of LNCS, pages 167-184, Nice, France, 1999. Springer. Google Scholar
  35. Freek Wiedijk. The Seventeen Provers of the World, volume 3600 of LNCS. Springer, Berlin, Heidelberg, 2006. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact