04/08/06: seplog milestone (ICFEM 2006)

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
• 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