Separation Logic
From MaRDI portal
- Computer science logic. 15th international workshop, CSL 2001, 10th annual conference of the EACSL, Paris, France, September 10--13, 2001. Proceedings
- Unnamed Publication
- Imperative Functional Programming with Isabelle/HOL
- Interactive theorem proving. First international conference, ITP 2010, Edinburgh, UK, July 11--14, 2010. Proceedings
- The Isabelle collections framework
- Theorem proving in higher order logics. 21st international conference, TPHOLs 2008, Montreal, Canada, August 18--21, 2008. Proceedings
- Verifying object-oriented programs with higher-order separation logic in Coq
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
