Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH scholarly article en Chen, Ran; Cohen, Cyril; LÚvy, Jean-Jacques; Merz, Stephan; ThÚry, Laurent http://www.dagstuhl.de/lipics License
when quoting this document, please refer to the following
DOI:
URN: urn:nbn:de:0030-drops-110683
URL:

; ; ; ;

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

pdf-format:


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.

BibTeX - Entry

@InProceedings{chen_et_al:LIPIcs:2019:11068,
  author =	{Ran Chen and Cyril Cohen and Jean-Jacques L{\'e}vy and Stephan Merz and Laurent Th{\'e}ry},
  title =	{{Formal Proofs of Tarjan's Strongly Connected Components Algorithm in Why3, Coq and Isabelle}},
  booktitle =	{10th International Conference on Interactive Theorem Proving (ITP 2019)},
  pages =	{13:1--13:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-122-1},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{141},
  editor =	{John Harrison and John O'Leary and Andrew Tolmach},
  publisher =	{Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{http://drops.dagstuhl.de/opus/volltexte/2019/11068},
  URN =		{urn:nbn:de:0030-drops-110683},
  doi =		{10.4230/LIPIcs.ITP.2019.13},
  annote =	{Keywords: Mathematical logic, Formal proof, Graph algorithm, Program verification}
}

Keywords: Mathematical logic, Formal proof, Graph algorithm, Program verification
Seminar: 10th International Conference on Interactive Theorem Proving (ITP 2019)
Issue date: 2019
Date of publication: 2019


DROPS-Home | Fulltext Search | Imprint | Privacy Published by LZI