Formalizing the Edmonds-Karp Algorithm

DOI10.1007/978-3-319-43144-4_14zbMATH Open1468.68327OpenAlexW2477881860MaRDI QIDQ2829260FDOQ2829260

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)

Cites Work

• Title not available (Why is that?)
• Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
• Maximal Flow Through a Network
• 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 (11)

• 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 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
• Title not available (Why is that?)
• Formalizing network flow algorithms: a refinement approach in Isabelle/HOL

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)