Edmonds-Karp
From MaRDI portal
- A Brief Overview of HOL4
- A formally verified compiler back-end
- A new approach to the maximum-flow problem
- A Powerdomain Construction
- A strong-connectivity algorithm and its applications in data flow analysis
- A theoretical basis for stepwise refinement and the programming calculus
- A transitive closure algorithm
- Adaptive solutions to the mutual exclusion problem
- Algorithms for dense graphs and networks on the random access computer
- Alternative Aggregates in Mizar
- An axiomatic basis for computer programming
- An O(n \text{log} n) implementation of the standard method for minimizing n-state finite automata
- Animating the formalised semantics of a Java-like language
- Applying data refinement for monadic programs to Hopcroft's algorithm
- Around Hopcroft’s Algorithm
- Automatic Data Refinement
- Bridging the Gap: Automatic Verified Abstraction of C
- Characteristic formulae for the verification of imperative programs
- Code generation via higher-order rewrite systems
- Compositional shape analysis by means of bi-abduction
- Construction of Büchi Automata for LTL Model Checking Verified in Isabelle/HOL
- Data Refinement
- Data refinement in Isabelle/HOL
- Depth-First Search and Linear Graph Algorithms
- Dinitz' algorithm: the original version and Even's version
- Efficient determination of the transitive closure of a directed graph
- Encoding, decoding and data refinement
- Enumeration and generation with a string automata representation
- Finger trees: a simple general-purpose data structure
- Formal Certification of a Resource-Aware Language Implementation
- Formalizing the Edmonds-Karp algorithm
- Formalizing the Logic-Automaton Connection
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Unnamed Publication
- Imperative Functional Programming with Isabelle/HOL
- Interpretation of Locales in Isabelle: Theories and Proof Contexts
- Introduction to algorithms.
- Isabelle/HOL. A proof assistant for higher-order logic
- Maximal Flow Through a Network
- Mechanised Separation Algebra
- Model Checking Software
- Modular compiler verification. A refinement-algebraic approach advocating stepwise abstraction
- More efficient on-the-fly LTL verification with Tarjan's algorithm
- Path-based depth-first search for strong and biconnected components
- Permission accounting in separation logic
- Program development by stepwise refinement
- Proof of correctness of data representations
- Proof-producing synthesis of ML from higher-order logic
- Reasoning about infinite computations
- Refinement Calculus
- Refinement concepts formalised in higher order logic
- Refinement to Imperative/HOL
- Secure Microkernels, State Monads and Scalable Refinement
- The B-Book
- The HOL-Omega Logic
- The Isabelle collections framework
- The new Quickcheck for Isabelle. Random, exhaustive and symbolic testing under one roof
- The normal number of prime factors of a number n.
- The smallest networks on which the Ford-Fulkerson maximum flow procedure may fail to terminate
- Theoretical Improvements in Algorithmic Efficiency for Network Flow Problems
- Theory Is Forever
- Three SCC-based emptiness checks for generalized Büchi automata
- Tools and Algorithms for the Construction and Analysis of Systems
- Toward a verified relational database management system
- Verified efficient implementation of Gabow's strongly connected component algorithm
Cited in
(28)- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
- Netsoft
- Refinement to imperative HOL
- A mechanized proof of the max-flow min-cut theorem for countable networks with applications to probability theory
- Graph theory in Coq: minors, treewidth, and isomorphisms
- Efficient verification of imperative programs using auto2
- Autoref
- CFML
- libclang
- MLton
- VACID-0
- GRAT
- Separation Logic
- Dijkstra Shortest Path
- Refinement Monadic
- Flow Networks
- Collections
- CAVA LTL Modelchecker
- Gabow SCC
- Imperative Refinement
- IEEE_Floating_Point
- Auto2_Imperative_HOL
- MFMC_Countable
- Prpu_Maxflow
- scientific article; zbMATH DE number 7649969 (Why is no real title available?)
- scientific article; zbMATH DE number 7649971 (Why is no real title available?)
- Efficient verified (UN)SAT certificate checking
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
This page was built for software: Edmonds-Karp
