> Details

Chen, Ran [Author]; Cohen, Cyril [Author]; Lévy, Jean-Jacques [Author]; Merz, Stephan [Author]; Théry, Laurent [Author] ; Ran Chen and Cyril Cohen and Jean-Jacques Lévy and Stephan Merz and Laurent Théry [Contributor]

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

Reference
management

Bookmarks

Remove from
bookmarks

Share this on Whatsapp

Close

Bookmarks



You can manage bookmarks using lists, please log in to your user account for this.
  • Media type: Text; E-Article; Electronic Conference Proceeding
  • Title: Formal Proofs of Tarjan’s Strongly Connected Components Algorithm in Why3, Coq and Isabelle
  • Contributor: Chen, Ran [Author]; Cohen, Cyril [Author]; Lévy, Jean-Jacques [Author]; Merz, Stephan [Author]; Théry, Laurent [Author]
  • Published: Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2019
  • Language: English
  • DOI: https://doi.org/10.4230/LIPIcs.ITP.2019.13
  • Keywords: Mathematical logic ; Graph algorithm ; Program verification ; Formal proof
  • Origination:
  • Footnote: Diese Datenquelle enthält auch Bestandsnachweise, die nicht zu einem Volltext führen.
  • Description: 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.
  • Access State: Open Access