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