A semi-automatic proof of strong connectivity

DOI10.1007/978-3-319-72308-2_4MaRDI QIDQ1630027zbMATH OpenOpenAlexFDO

Authors Ran Chen, Jean-Jacques Lévy

Publication date 7 December 2018

Full work available at URL https://hal.inria.fr/hal-01632947/file/17scct.pdf

Mathematics Subject Classification ID

Directed graphs (digraphs), tournaments (05C20) Connectivity (05C40) Software, source code, etc. for problems pertaining to combinatorics (05-04)

Recommendations

• Verified efficient implementation of Gabow's strongly connected component algorithm
• A simplified correctness proof for a well-known algorithm computing strongly connected components.
• Why3 -- where programs meet provers
• On finding the strongly connected components in a directed graph
• scientific article; zbMATH DE number 5879017

Cited in

(6)

• Verified efficient implementation of Gabow's strongly connected component algorithm
• FEMaLeCoP: Fairly Efficient Machine Learning Connection Prover
• A formally proved, complete algorithm for path resolution with symbolic links
• scientific article; zbMATH DE number 7649967 (Why is no real title available?)
• scientific article; zbMATH DE number 7649962 (Why is no real title available?)
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL

Describes a project that uses

Uses Software

• Coq
• Why3
• Coq/SSReflect

This page was built for publication: A semi-automatic proof of strong connectivity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1630027)