Mechanized Program Verification and Analysis with Separation Logic

Several tools have been developed for mechanizing separation logic proofs, ranging from interactive tools to fully automatic tools. This page focuses on more automatic approaches. For the other end of the spectrum, go to:

Semi-automatic verification tools

Tools in this category typically require user-provided pre/post specifications for each function, loop invariants, and resource invariants for concurrent programs. First steps in this direction were taken in the Smallfoot project (2002-2005).

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

Symbolic execution is based on solving the frame inference problem: Given $P$ and $Q$ find the strongest assertion $F$ such that $P \vdash Q * F$ if one exists, or fail otherwise. For efficiency and/or decidability reasons, the provers often return slightly weaker assertions and may even fail to prove valid entailments.

Other tools

Automatic verification tools

Tools in this category do not require any annotations except perhaps for the specification of the program to be verified. The tools are responsible for finding suitable loop invariants and, in case of concurrent programs, also resource invariants or rely-guarantee conditions.

These tools infer invariants via a fixed-point calculation in a suitable abstract domain, in the usual manner of abstract interpretation. Some results in this area are:

ToolSupport (last edited 2011-02-07 14:28:53 by viktor)