Cited in
(32)- Transition_Systems_and_Automata
- A verified ODE solver and the Lorenz attractor
- Verified efficient implementation of Gabow's strongly connected component algorithm
- Formalizing the Edmonds-Karp algorithm
- Verifying Faradžev-Read Type Isomorph-Free Exhaustive Generation
- Formal verification of an executable LTL model checker with partial order reduction
- Netsoft
- Autoref
- CFML
- MLton
- CAVA Automata Library
- CAVA
- Dijkstra Shortest Path
- Edmonds-Karp
- Collections
- Flow Networks
- Affine Arithmetic
- CAVA LTL Modelchecker
- Dictionary Construction
- Separation Logic
- Gabow SCC
- LTL_to_DRA
- Native Word
- Imperative Refinement
- Stuttering Equivalence
- Program-Conflict-Analysis
- Boolean_Expression_Checkers
- Prpu_Maxflow
- scientific article; zbMATH DE number 7649962 (Why is no real title available?)
- scientific article; zbMATH DE number 7649960 (Why is no real title available?)
- Refinement to imperative HOL
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
This page was built for software: Refinement Monadic