Formalizing Push-Relabel Algorithms
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
- On implementing the push-relabel method for the maximum flow problem
- 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
This page was built for software: Formalizing Push-Relabel Algorithms
