NB: See this page ("seplog" tab) 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
- Some generic tactics: util_tactic.v (include an improvement of omega for Z)
- Definition of heaps as a module: heap.v
- Tactics for heaps: heap_tactic.v (includes the tactics Disjoint_heap and Equal_heap to prove separating conjunction goals)
- Expression and assertion language: bipl.v
- Operational and axiomatic semantics: axiomatic.v
- A weakest-precondition generator: vc.v
- Some reusable lemmas: contrib.v
- Some reusable tactics: contrib_tactics.v (includes the tactics Frame_rule)
- Some sample verifications: examples.v, example_reverse_list.v
- Automatic tactic for a fragment of separation logic: omega_test.v, frag.v, frag_examples.v

- Verification of Topsy Memory Isolation:
- Definitions of heap-lists and their properties: topsy_hm.v
- The initialization function (using the automatic tactic): topsy_hmInit.v
- The allocation function: topsy_hmAlloc.v
- The deallocation function: topsy_hmFree.v
- Example using the Hoare triple for hmAlloc: hmAlloc_example.v

- Definitions of heap-lists and their properties: topsy_hm.v
- New specification for hmAlloc (precise post-condition for allocation success): topsy_hmAlloc2.v
- Compilation:
- Header file: seplog_header.v
- Building script: build
- Cleaning script: clean