Separation Logic Implementation in Coq

Technical documents

• A Certified Verifier for a Fragment of Separation Logic, Nicolas Marti, Reynald Affeldt, Computer Software 25(3):135-147, 2008 (also available online through J-STAGE, an early version of this paper was presented at the PPL 2007 workshop where it received the Best Paper Award)
• Formal Verification of the heap manager of an operating system using separation logic, Nicolas Marti, Reynald Affeldt, and Akinori Yonezawa, ICFEM 2006, vol. 4260 of Lecture Notes in Computer Science, p. 400-419 (revised version of our SPACE 2006 paper, slides)
  
• Early overview paper (presented at the JSSST 2005 workshop, slides)

See here for further information.

Bigtoe: A Certified Verifier for a Fragment of Separation Logic

• Interactive demo based on the extracted OCaml code.

Coq Implementation Overview

The whole archive: seplog.tgz, CVS browser (As of August 2007, a more recent version is available here)

• 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
• Tactic by Reflection for proving separation logic triples
  • Certified decision procedure for Presburger Arithmetic (based on Fourier-Motzkin lemma): expr_b_dp.v
  • Verification condition generator: frag_list_vcg.v
  • Transformation from triples to entailment: frag_list_triple.v
  • Entailment verification: frag_list_entail.v
  • Some examples: frag_list_examples.v
• Topsy Heap Manager Verification:
  • 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
• Compilation:
  • Header file: seplog_header.v
  • Building script: build
  • Cleaning script: clean

Contact information: reynald dot affeldt at aist dot go dot jp