04/08/06: seplog milestone (ICFEM 2006)
NB: See this page ("seplog" tab) for an updated version.
The Coq code corresponding to this paper.
- Encoding of Separation logic:
- Verification of Topsy Memory Isolation:
- Definitions of heap-lists and their properties: topsy_hm.v
- New specification for hmAlloc (precise post-condition for allocation success): topsy_hmAlloc2.v