10/01/06: seplog milestone (SPACE 2006)
The whole archive: space06.tar.gz
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:
- Compilation: