Formalizing network flow algorithms: a refinement approach in Isabelle/HOL

DOI10.1007/s10817-017-9442-4zbMath1468.68328OpenAlexW2775427311MaRDI QIDQ1722647

Peter Lammich, S. Reza Sefidgar

Publication date: 18 February 2019

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://www.research.manchester.ac.uk/portal/en/publications/formalizing-network-flow-algorithms-a-refinement-approach-in-isabellehol(b8fb5906-1351-4c19-b6c0-b858b5888832).html

zbMATH Keywords

stepwise refinementformal verificationIsabelle/HOLmaximum flow problemEdmonds-Karp algorithmpush-relabel algorithm

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 (7)

Local Reasoning for Global Graph Properties ⋮ Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms ⋮ Unnamed Item ⋮ From LCF to Isabelle/HOL ⋮ Trustworthy Graph Algorithms (Invited Talk) ⋮ Prpu_Maxflow ⋮ A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory

Uses Software

• Coq
• Isabelle
• Isabelle/HOL
• Why3
• Isar
• Netsoft
• HOL
• DIMACS
• WhyML
• MLton
• GitHub
• Edmonds-Karp
• Separation Logic
• Dijkstra Shortest Path
• Refinement Monadic
• Flow Networks
• Amortized Complexity
• Archive Formal Proofs
• Gabow SCC

Cites Work

• Unnamed Item
• Unnamed Item
• The smallest networks on which the Ford-Fulkerson maximum flow procedure may fail to terminate
• Partial and nested recursive function definitions in higher-order logic
• On implementing the push-relabel method for the maximum flow problem
• Isabelle/HOL. A proof assistant for higher-order logic
• A semi-automatic proof of strong connectivity
• A graph library for Isabelle
• Formalizing the Edmonds-Karp Algorithm
• 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
• Machine-Checked Verification of the Correctness and Amortized Complexity of an Efficient Union-Find Implementation
• Refinement to Imperative/HOL
• Amortized Complexity Verified
• 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
• Why3 — Where Programs Meet Provers
• Alternative Aggregates in Mizar
• Program development by stepwise refinement

This page was built for publication: Formalizing network flow algorithms: a refinement approach in Isabelle/HOL