NB: See this page for an updated version.

The Coq code corresponding to this paper.

Contents overview:

- Encoding of Separation logic:
- Some generic lemmas about integers, lists, etc.: util.v
- Definition of heaps as a module: heap.v
- Expression and assertion language: bipl.v (includes a tactic to solve separating conjunction goals)
- Operational and axiomatic semantics: axiomatic.v
- A weakest-precondition generator: vc.v
- Some reusable lemmas: contrib.v
- Some sample verifications: examples.v, example_reverse_list.v

- Verification of Topsy Memory Isolation:
- Global definitions for the heap manager (heap-list and basic lemmas): topsy_hm.v
- The initialization function: topsy_hmInit.v
- The allocation function: topsy_hmAlloc.v
- The deallocation function: topsy_hmFree.v

- The initialization function of the thread manager: topsy_threadBuild.v
- The bootloader (in progress): topsy_bootloader.v

- Global definitions for the heap manager (heap-list and basic lemmas): topsy_hm.v
- Compilation:
- Header file: seplog_header.v
- Building script: build
- Cleaning script: clean