Separation Logic
From MaRDI portal
swMATH28549MaRDI QIDQ40263FDOQ40263
Author name not available (Why is that?)
Official website: https://www.isa-afp.org/entries/Separation_Logic_Imperative_HOL.html
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
- Refinement to Imperative/HOL
- 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
- Verifying asymptotic time complexity of imperative programs in Isabelle
- PLM
- Prpu_Maxflow
- Matroids
- Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits
- Formalizing the Edmonds-Karp algorithm
- Formalizing network flow algorithms: a refinement approach in Isabelle/HOL
This page was built for software: Separation Logic
