Verified efficient implementation of Gabow's strongly connected component algorithm

DOI10.1007/978-3-319-08970-6_21MaRDI QIDQ2879261zbMATH OpenOpenAlexFDO

Authors Peter Lammich

Publication date 8 September 2014

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-08970-6_21

Mathematics Subject Classification ID

Directed graphs (digraphs), tournaments (05C20) Connectivity (05C40) Graph algorithms (graph-theoretic aspects) (05C85)

Recommendations

• A semi-automatic proof of strong connectivity
• A simplified correctness proof for a well-known algorithm computing strongly connected components.
• An algorithm for strongly connected component analysis in \(n \log n\) symbolic steps
• Verification of the Schorr-Waite algorithm -- from trees to graphs
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL

Cited in

(20)

• I/O- and CPU-optimal recognition of strongly connected components
• A semi-automatic proof of strong connectivity
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• Refinement to imperative HOL
• A simplified correctness proof for a well-known algorithm computing strongly connected components.
• From LCF to Isabelle/HOL
• Automatic refinement to efficient data structures: a comparison of two approaches
• Formalizing the Edmonds-Karp algorithm
• Refinement to Imperative/HOL
• Verification of the Schorr-Waite algorithm -- from trees to graphs
• Gabow SCC
• Trustworthy Graph Algorithms (Invited Talk)
• scientific article; zbMATH DE number 7649960 (Why is no real title available?)
• scientific article; zbMATH DE number 7649962 (Why is no real title available?)
• scientific article; zbMATH DE number 7649967 (Why is no real title available?)
• scientific article; zbMATH DE number 7649969 (Why is no real title available?)
• Efficient verified (UN)SAT certificate checking
• Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting
• Formal verification of an executable LTL model checker with partial order reduction
• Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms

Describes a project that uses

Uses Software

• Isabelle
• ML
• Isabelle/HOL
• HOL
• Refinement Monadic
• Collections
• Archive Formal Proofs
• Native Word

This page was built for publication: Verified efficient implementation of Gabow's strongly connected component algorithm

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