Mechanized Program Verification and Analysis with Separation Logic

 

Tools and Projects


Automatic (or nearly)

  1. -Smallfoot (London)

  2. -Space Invader (London)

  3. -SLAyer (Microsoft)

  4. -SmallfootRG (Ldn+Cambridge)

  5. -Hip (Singapore)

  6. -JStar (London+Cambridge)

  7. -Verifast (Leuven, Belgium)

  8. -Vericool (Leuven, Belgium)

  9. -Thor (CMU)

  10. -HeapHop (ENS Paris)

  11. -Xisa (Boulder+Paris+Berkeley)


Interactive

  1. -Holfoot (Cambridge)

  2. -Ynot (Harvard)

  3. -Concurrent C Minor (Princeton)

  4. -Compcert (Inria Paris-Roquencourt)

  5. -Flint (Yale)

  6. -certified verifier  (Tokyo)

  7. -L4.verified (Sydney)

Automatic. First steps were taken in the Smallfoot project (2002-2005).

  1. -Symbolic Execution with Separation Logic. J Berdine, C Calcagno and PW O'Hearn. Proceedings of APLAS'05, LNCS 3780, pp52-68.

  2. -Smallfoot: Modular Automatic Assertion Checking with Separation Logic J Berdine, C Calcagno and PW O'Hearn. In 4th FMCO, LNCS 4111, 2006

Smallfoot did verification by symbolic execution interspersed with entailment checking, rather than the ``vcgen’’ method. Formulae were updated in-place, which obviated the need for complex alias checking. The other significant point was an automatic technique for inferring frame axioms.


Smallfoot did automatic proofs of lightweight safety properties of programs, mimicking the proofs done by hand in most of the early separation logic papers, up to and including Concurrent Separation Logic. It requires loop invariants, pre/post specs, and resource invariants for concurrent programs. Later program analysis tools found ways to infer these annotations, when verifying considerably less than functional correctness.


The next step, done by two groups independently, was to use symbolic execution together with selected true implications to infer invariants via a fixed-point calculation, in the usual manner of abstract interpretation.

  1. -A local shape analysis based on separation logic D Distefano, P O'Hearn and H Yang. In 12th TACAS, LNCS 3920, pp287-302, 2006.

  2. -Inferring invariants in Separation Logic for imperative list-processing algorithms. S Magill, A Nanevsky, E Clarke and P Lee, SPACE 2006

There are lots of papers and a number of tools on automatic verification and analysis using separation logic, and there is lots of variation on the kinds of properties checked and the degree of automation. There are emphases on numerical properties (THOR, Hip), Concurrency (SmallfootRG, HeapHop, Verifast), on integration with SMT solvers and properties edging towards functional correctness (Verifast, Hip), on stronger shape properties and higher automation (Space Invader, SLAyer, Xisa), and OOP (jStar, Hip, Vericool). There are also further algorithmic ideas, such as for synthesis of resource invariants in concurrent programs (here and here), and methods that adapt the analysis by guessing data structure definitions (here and here).

Some practical highlights include the first automatic proofs of pointer usage in entire industrial programs, Microsoft and Linux device drivers of up to 10K LOC

  1. -Scalable Shape Analysis for Systems Code. H Yang, O Lee, J Berdine, C Calcagno, B Cook, D Distefano and P O'Hearn. In CAV'08 .

and a way to infer procedure specs without knowing any preconditions or the procedure’s callers, opening the way to application to much bigger programs than before (> 1M LOC), with way less lead-up time to get the analysis ready

  1. -Compositional Shape Analysis by means of Bi-Abduction
    C Calcagno, D Distefano, PW O'Hearn and H Yang.
    POPL'09 .



Interactive. On the other hand, it is incredibly difficult for fully automatic techniques to prove full functional correctness. A number of projects, again in the toolbar to the right, use separation logic within a proof assistant (in the sense of the LCF/HOL/Isabelle/Coq tradition). There are some impressive proofs that have been done, and I will be updating this information soon.