Formalizing the Edmonds-Karp algorithm

DOI10.1007/978-3-319-43144-4_14MaRDI QIDQ2829260zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

Programming involving graphs or networks (90C35) Analysis of algorithms (68W40) Flows in graphs (05C21) Formalization of mathematics in connection with theorem provers (68V20)

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

Cites work

• A graph library for Isabelle
• A new approach to the maximum-flow problem
• Alternative Aggregates in Mizar
• Applying data refinement for monadic programs to Hopcroft's algorithm
• Bridging the Gap: Automatic Verified Abstraction of C
• Characteristic formulae for the verification of imperative programs
• Code generation via higher-order rewrite systems
• Imperative Functional Programming with Isabelle/HOL
• Interpretation of Locales in Isabelle: Theories and Proof Contexts
• Introduction to algorithms.
• Maximal Flow Through a Network
• Program development by stepwise refinement
• Refinement Calculus
• Refinement to Imperative/HOL
• The smallest networks on which the Ford-Fulkerson maximum flow procedure may fail to terminate
• Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems
• Verified efficient implementation of Gabow's strongly connected component algorithm

Cited in

(13)

• Refinement of parallel algorithms down to LLVM: applied to practically efficient parallel sorting
• Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
• Graph theory in Coq: minors, treewidth, and isomorphisms
• A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
• Efficient verified (UN)SAT certificate checking
• Edmonds-Karp
• A parallel realization of the Edmonds-Karp algorithm
• A survivable variant of the ring star problem
• Paralleling of Edmonds-Karp network flow algorithm
• scientific article; zbMATH DE number 7649969 (Why is no real title available?)
• Refinement to imperative HOL
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)

Describes a project that uses

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• Isar
• HOL
• Separation Logic
• Dijkstra Shortest Path
• Refinement Monadic
• Archive Formal Proofs
• Gabow SCC

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)