Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle

Cyril Cohen (MARELLE); Jean-Jacques Levy (PI.R2); Laurent Thery (MARELLE); Ran Chen; Stephan Merz (VERIDIS)

arxiv: 1810.11979 · v1 · pith:7T2BSDJ6new · submitted 2018-10-29 · 💻 cs.LO

Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle

Ran Chen , Cyril Cohen (MARELLE) , Jean-Jacques Levy (PI.R2) , Stephan Merz (VERIDIS) , Laurent Thery (MARELLE) This is my paper

classification 💻 cs.LO

keywords algorithmformalisabelleproofwhy3alwaysassistantscarried

0 comments

read the original 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.

This paper has not been read by Pith yet.

Formal Proofs of Tarjan's Algorithm in Why3, Coq, and Isabelle

discussion (0)