Formalizing the Edmonds-Karp Algorithm

DOI10.1007/978-3-319-43144-4_14zbMath1468.68327OpenAlexW2477881860MaRDI QIDQ2829260

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)

Related Items

Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms, Unnamed Item, Unnamed Item, A survivable variant of the ring star problem, Graph theory in Coq: minors, treewidth, and isomorphisms, Formalizing network flow algorithms: a refinement approach in Isabelle/HOL, Refinement to imperative HOL, Efficient verified (UN)SAT certificate checking, Edmonds-Karp, A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory

Uses Software

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

Cites Work

• Unnamed Item
• The smallest networks on which the Ford-Fulkerson maximum flow procedure may fail to terminate
• A graph library for Isabelle
• Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
• Bridging the Gap: Automatic Verified Abstraction of C
• Applying Data Refinement for Monadic Programs to Hopcroft’s Algorithm
• Refinement to Imperative/HOL
• Maximal Flow Through a Network
• Imperative Functional Programming with Isabelle/HOL
• Code Generation via Higher-Order Rewrite Systems
• A new approach to the maximum-flow problem
• Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems
• Refinement Calculus
• Characteristic formulae for the verification of imperative programs
• Alternative Aggregates in Mizar
• Program development by stepwise refinement
• Interpretation of Locales in Isabelle: Theories and Proof Contexts