Formalizing the Edmonds-Karp algorithm
DOI10.1007/978-3-319-43144-4_14zbMATH Open1468.68327OpenAlexW2477881860MaRDI QIDQ2829260FDOQ2829260
Authors: Peter Lammich, S. Reza Sefidgar 
Publication date: 27 October 2016
Published in: Interactive Theorem Proving (Search for Journal in Brave)
Full work available at URL: https://www.research.manchester.ac.uk/portal/en/publications/formalizing-the-edmondskarp-algorithm(f7a74014-3a83-46de-b212-1678ad8e145e).html
Recommendations
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- A parallel realization of the Edmonds-Karp algorithm
- Paralleling of Edmonds-Karp network flow algorithm
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
- A new approach to the maximum-flow problem
Programming involving graphs or networks (90C35) Analysis of algorithms (68W40) Flows in graphs (05C21) Formalization of mathematics in connection with theorem provers (68V20)
Cites Work
- Verified efficient implementation of Gabow's strongly connected component algorithm
- Maximal Flow Through a Network
- Introduction to algorithms.
- Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems
- Refinement Calculus
- A new approach to the maximum-flow problem
- Characteristic formulae for the verification of imperative programs
- Program development by stepwise refinement
- Bridging the Gap: Automatic Verified Abstraction of C
- The smallest networks on which the Ford-Fulkerson maximum flow procedure may fail to terminate
- Code generation via higher-order rewrite systems
- Imperative Functional Programming with Isabelle/HOL
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
- Applying data refinement for monadic programs to Hopcroft's algorithm
- Refinement to Imperative/HOL
- A graph library for Isabelle
- Alternative Aggregates in Mizar
Cited In (13)
- Graph theory in Coq: minors, treewidth, and isomorphisms
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
- Refinement to imperative HOL
- Efficient verified (UN)SAT certificate checking
- Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting
- Title not available (Why is that?)
- A parallel realization of the Edmonds-Karp algorithm
- A survivable variant of the ring star problem
- Edmonds-Karp
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
- Paralleling of Edmonds-Karp network flow algorithm
- Title not available (Why is that?)
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
Uses Software
This page was built for publication: Formalizing the Edmonds-Karp algorithm
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829260)
