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

DOI10.1007/S10817-017-9442-4MaRDI QIDQ1722647zbMATH OpenOpenAlexFDO

Authors 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

formal verificationIsabelle/HOLmaximum flow problemstepwise refinementEdmonds-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)

Recommendations

• Formalization of Data Flow Computing and a Coinductive Approach to Verifying Flowware Synthesis
• Guarded second-order logic, spanning trees, and network flows
• Publication:4723281
• scientific article; zbMATH DE number 1852172
• Network flow and 2-satisfiability
• Experimenting Formal Proofs of Petri Nets Refinements
• Computational verification of network programs in Coq

Cites work

• scientific article; zbMATH DE number 487935 (Why is no real title available?)
• A graph library for Isabelle
• A new approach to the maximum-flow problem
• A semi-automatic proof of strong connectivity
• Alternative Aggregates in Mizar
• Amortized complexity verified
• 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
• Formalizing the Edmonds-Karp algorithm
• Imperative Functional Programming with Isabelle/HOL
• Introduction to algorithms.
• Isabelle/HOL. A proof assistant for higher-order logic
• Machine-checked verification of the correctness and amortized complexity of an efficient union-find implementation
• Maximal Flow Through a Network
• On implementing the push-relabel method for the maximum flow problem
• Partial and nested recursive function definitions in higher-order logic
• 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
• Why3 -- where programs meet provers

Cited in

(10)

• Verified efficient implementation of Gabow's strongly connected component algorithm
• 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
• From LCF to Isabelle/HOL
• Formalizing the Edmonds-Karp algorithm
• A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
• Prpu_Maxflow
• Local reasoning for global graph properties
• Trustworthy Graph Algorithms (Invited Talk)
• scientific article; zbMATH DE number 7649971 (Why is no real title available?)

Describes a project that uses

Uses Software

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

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

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q1722647)