Cited in
(35)- Efficient verification of imperative programs using auto2
- Verifying the Correctness of Disjoint-Set Forests with Kleene Relation Algebras
- Refinement to imperative HOL
- For a few dollars more. Verified fine-grained algorithm analysis down to LLVM
- Netsoft
- Ynot
- CFML
- MLton
- AUTO2
- Grail
- CSimpl
- Camelot
- AVL trees
- Amortized Complexity
- TiML
- Dijkstra Shortest Path
- Edmonds-Karp
- Collections
- Flow Networks
- Refinement Monadic
- Gabow SCC
- VST-Floyd
- Imperative Refinement
- Stone Algebras
- Landau Symbols
- Median-of-Medians
- Auto2_Imperative_HOL
- PLM
- Prpu_Maxflow
- Refinement to Imperative/HOL
- Verifying asymptotic time complexity of imperative programs in Isabelle
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
- Matroids
- Formalizing the Edmonds-Karp algorithm
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
This page was built for software: Separation Logic
