Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm

DOI10.1007/978-3-319-08970-6_21zbMath1416.68168OpenAlexW91886818MaRDI QIDQ2879261

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

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

Related Items

Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms, Refinement to Imperative/HOL, Automatic refinement to efficient data structures: a comparison of two approaches, Unnamed Item, Unnamed Item, Unnamed Item, Unnamed Item, Formalizing network flow algorithms: a refinement approach in Isabelle/HOL, Refinement to imperative HOL, Formal verification of an executable LTL model checker with partial order reduction, From LCF to Isabelle/HOL, Efficient verified (UN)SAT certificate checking, Gabow SCC, Formalizing the Edmonds-Karp Algorithm

Uses Software

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