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 metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-01632947
Contributor : Claude Marché <>
Submitted on : Friday, November 10, 2017 - 5:51:21 PM
Last modification on : Wednesday, September 16, 2020 - 5:26:30 PM
Long-term archiving on: : Sunday, February 11, 2018 - 3:19:13 PM

File

17scct.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01632947, version 1

Citation

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⟩

Share

Metrics

Record views

765

Files downloads

325