Cited in
(37)- Formal verification of an executable LTL model checker with partial order reduction
- Functional correctness of C implementations of Dijkstra's, Kruskal's, and Prim's algorithms
- Refinement to imperative HOL
- Efficient verified (UN)SAT certificate checking
- Netsoft
- Autoref
- CFML
- MLton
- Fiat
- CAMPY
- VACID-0
- CAVA Automata Library
- CAVA
- Dijkstra Shortest Path
- Edmonds-Karp
- Collections
- Flow Networks
- Graph Theory
- CAVA LTL Modelchecker
- Refinement Monadic
- Separation Logic
- LTL_to_DRA
- Native Word
- Imperative Refinement
- LTL_to_GBA
- Stuttering Equivalence
- Real_Impl
- Tree Automata
- Program-Conflict-Analysis
- Dune
- Boolean_Expression_Checkers
- Prpu_Maxflow
- Transition_Systems_and_Automata
- From LCF to Isabelle/HOL
- Automatic refinement to efficient data structures: a comparison of two approaches
- Formalizing the Edmonds-Karp algorithm
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
This page was built for software: Gabow SCC
