2026-08-18T12:52:28Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:11068 2024-03-12T12:01:59Z ddc:004 open_access

Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle Chen, Ran Cohen, Cyril Lévy, Jean-Jacques Merz, Stephan Théry, Laurent Mathematical logic Formal proof Graph algorithm Program verification 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. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Ran Chen and Cyril Cohen and Jean-Jacques Lévy and Stephan Merz and Laurent Théry 2019 Is Part Of LIPIcs, Volume 141, 10th International Conference on Interactive Theorem Proving (ITP 2019) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.ITP.2019.13 urn:nbn:de:0030-drops-110683 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2019.13 eng https://creativecommons.org/licenses/by/3.0/legalcode