Formal Proofs of Tarjan\u27s Strongly Connected Components Algorithm in Why3, Coq and Isabelle
- Chen, Ran
- Cohen, Cyril
- Merz, Stephan
Publication date
January 2019
DOI Publisher
LIPIcs - Leibniz International Proceedings in Informatics. 10th International Conference on Interactive Theorem Proving (ITP 2019) Language
EnglishAbstract
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
Add to ORKG