10/01/06: seplog milestone (SPACE 2006)

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
• Compilation:
  • Header file: seplog_header.v
  • Building script: build
  • Cleaning script: clean