Verified efficient implementation of Gabow's strongly connected component algorithm
From MaRDI portal
Publication:2879261
DOI10.1007/978-3-319-08970-6_21zbMATH Open1416.68168OpenAlexW91886818MaRDI QIDQ2879261FDOQ2879261
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
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
Directed graphs (digraphs), tournaments (05C20) Graph algorithms (graph-theoretic aspects) (05C85) Connectivity (05C40)
Cited In (18)
- Title not available (Why is that?)
- A simplified correctness proof for a well-known algorithm computing strongly connected components.
- 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
- Refinement to imperative HOL
- Formalizing the Edmonds-Karp Algorithm
- Efficient verified (UN)SAT certificate checking
- I/O- and CPU-optimal recognition of strongly connected components
- Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting
- Refinement to Imperative/HOL
- Gabow SCC
- From LCF to Isabelle/HOL
- Title not available (Why is that?)
- Automatic refinement to efficient data structures: a comparison of two approaches
- Verification of the Schorr-Waite algorithm -- from trees to graphs
- Title not available (Why is that?)
- Title not available (Why is that?)
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
Uses Software
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)
