Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle
- Chen, Ran
- Cohen, Cyril
- Levy, Jean-Jacques
- Merz, Stephan
- Théry, Laurent
Publication date
September 2019
DOI Publisher
Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r InformatikAbstract
International audienceComparing provers on a formalization of the same problem is always a valuable exercise. In thispaper, we present the formal proof of correctness of a non-trivial algorithm from graph theory thatwas carried out in three proof assistants: Why3,Coq, and Isabelle
Add to ORKG