Skip to Main content Skip to Navigation
Conference papers

A Semi-automatic Proof of Strong connectivity

Ran Chen 1, 2 Jean-Jacques Lévy 3
1 TOCCATA - Formally Verified Programs, Certified Tools and Numerical Computations
LRI - Laboratoire de Recherche en Informatique, Inria Saclay - Ile de France
3 PI.R2 - Design, study and implementation of languages for proofs and programs
UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale, Inria de Paris
Abstract : We present a formal proof of the classical Tarjan-1972 algorithm for finding strongly connected components in directed graphs. We use the Why3 system to express these proofs and fully check them by computer. The Why3-logic is a simple multi-sorted first-order logic augmented by inductive predicates. Furthermore it provides useful libraries for lists and sets. The Why3 system allows the description of programs in a Why3-ML programming language (a first-order programming language with ML syntax) and provides interfaces to various state-of-the-art automatic provers and to manual interactive proof-checkers (we use mainly Coq). We do not claim that this proof is new, although we could not find a formal proof of that algorithm in the literature. But one important point of our article is that our proof is here completely presented and human readable.
Document type :
Conference papers
Complete list of metadata

Cited literature [26 references]  Display  Hide  Download
Contributor : Claude Marché Connect in order to contact the contributor
Submitted on : Friday, November 10, 2017 - 5:51:21 PM
Last modification on : Friday, January 21, 2022 - 3:19:29 AM
Long-term archiving on: : Sunday, February 11, 2018 - 3:19:13 PM


Files produced by the author(s)


  • HAL Id : hal-01632947, version 1


Ran Chen, Jean-Jacques Lévy. A Semi-automatic Proof of Strong connectivity. 9th Working Conference on Verified Software: Theories, Tools and Experiments (VSTTE), Jul 2017, Heidelberg, Germany. ⟨hal-01632947⟩



Les métriques sont temporairement indisponibles