Differences between revisions 1 and 12 (spanning 11 versions)
⇤ ← Revision 1 as of 2011-02-03 18:51:06 →
Size: 4168
Editor: viktor
Comment:
← Revision 12 as of 2011-02-07 14:28:53 → ⇥
Size: 4746
Editor: viktor
Comment:
Deletions are marked like this. Additions are marked like this.
Line 3: Line 3:
Several tools have been developed for mechanizing separation logic proofs. These range from fully automatic tools (where user provides no specification or perhaps only a very short specification of the entire program) and semi-automatic (where the user provides extensive specifications and loop invariants) to interactive (where the user does the entire part of the proof in an interactive theorem prover, such as Coq or Isabelle possibly assisted by advanced tactics to carry out mundane proof steps). 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:
Line 5: Line 5:
 * [[SLInProofAssistants|Separation logic in proofs assistants]]
Line 6: Line 7:
== Semi-automatic and Automatic == == Semi-automatic verification tools ==
Line 8: Line 9:
First steps were taken in the Smallfoot project (2002-2005). 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).
Line 10: Line 11:
 * Symbolic Execution with Separation Logic. J Berdine, C Calcagno and PW O'Hearn. APLAS 2005, LNCS 3780, pp52-68.
 * 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.		  * [[http://www.eecs.qmul.ac.uk/~ohearn/papers/execution_preprint.pdf|Symbolic Execution with Separation Logic.]] J Berdine, C Calcagno and PW O'Hearn. In APLAS 2005, LNCS 3780.
 * [[http://www.eecs.qmul.ac.uk/~ohearn/papers/smallfoot_v0.1.pdf|Smallfoot: Modular Automatic Assertion Checking with Separation Logic.]] J Berdine, C Calcagno and PW O'Hearn. In FMCO 2006, LNCS 4111.
Line 14: Line 14:
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. 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.
Line 16: Line 16:
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.
 * A local shape analysis based on separation logic D Distefano, P O'Hearn and H Yang. In 12th TACAS, LNCS 3920, pp287-302, 2006.
 * 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, Verifast). 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). 		Symbolic execution is based on solving the frame inference problem: Given <<latex($P$)>> and <<latex($Q$)>> find the strongest assertion <<latex($F$)>> such that <<latex($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.
Line 21: Line 18:
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
 * 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
 * Compositional Shape Analysis by means of Bi-Abduction. C Calcagno, D Distefano, PW O'Hearn and H Yang. POPL 2009.		 ==== Other tools ====
Line 26: Line 20:
==== Concurrency ====  * [[http://www.lsv.ens-cachan.fr/~villard/heaphop/|Heap-Hop]] (Paris): Smallfoot extension for message-passing programs.
 * [[http://loris-7.ddns.comp.nus.edu.sg/~project/hip/|Hip]] (Singapore)
 * [[http://www.jstarverifier.org/|jStar]] (London/Cambridge): SL-based verifier for Java programs.
 * [[http://www.cl.cam.ac.uk/~vv216/smallfootRG/|SmallfootRG]] (Cambridge): Smallfoot extension for fine-grained concurrent algorithms.
 * [[http://people.cs.kuleuven.be/~bart.jacobs/verifast/|Verifast]] (Leuven): verifier for Java and C.
Line 28: Line 26:
* [[http://www.mpi-sws.org/~viktor/cave/|CAVE]]: linearizability of fine-grained concurrent algorithms
* [[http://www.lsv.ens-cachan.fr/~villard/heaphop/|Heap-Hop]]: memory safety of message-passing programs
* [[http://www.cl.cam.ac.uk/~vv216/smallfootRG/|SmallfootRG]]: memory safety of fine-grained concurrent algorithms		 == Automatic verification tools ==
Line 32: Line 28:
== Interactive == 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.
Line 34: Line 30:
On the other hand, it is incredibly difficult for fully automatic techniques to prove full functional correctness. A number of projects use separation logic within a proof assistant (in the sense of the LCF/HOL/Isabelle/Coq tradition).  * [[http://www.mpi-sws.org/~viktor/cave/|CAVE]] (Cambridge/Kaiserslautern): verifies linearizability of fine-grained concurrent algorithms (using a variety of techniques in addition to SL).
 * [[http://www.eastlondonmassive.org/Home.html|Space Invader]] (London)
 * [[http://research.microsoft.com/en-us/um/cambridge/projects/slayer/|SLAyer]] (Cambridge): MS Windows device drivers.
 * [[http://www.cs.cmu.edu/~smagill/thor/|THOR]] (Pittsburgh): generates integer programs abstracting the SL proof.
 * [[http://xisa.cs.colorado.edu/|Xisa]] (Colorado/Paris): supports user-defined inductive data structures.

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:

 * [[http://www.eecs.qmul.ac.uk/~ohearn/papers/localshape.pdf|A local shape analysis based on separation logic.]] D Distefano, P O'Hearn and H Yang. In TACAS 2006, LNCS 3920, pp287-302.<<BR>>This paper introduces the domain of singly linked non-empty list segments.

 * [[http://www.eecs.qmul.ac.uk/~ohearn/papers/scalable.pdf|Scalable Shape Analysis for Systems Code]]. H Yang, O Lee, J Berdine, C Calcagno, B Cook, D Distefano and P O'Hearn. CAV 2008.<<BR>>This paper shows a carefully designed join operation for scaling shape analysis to entire Microsoft and Linux device drivers of up to 10K LOC.

 * [[http://www.eecs.qmul.ac.uk/~ohearn/papers/popl09.pdf|Compositional Shape Analysis by means of Bi-Abduction.]] C Calcagno, D Distefano, PW O'Hearn and H Yang. POPL 2009.<<BR>>This paper extends the frame inference question to a bi-abductive inference question: Given <<latex($P$)>> and <<latex($Q$)>> find <<latex($F$)>> (the frame) and <<latex($A$)>> (the anti-frame) such that <<latex($P * A \vdash Q * F$)>>. The paper describes an ordering on the solutions to this problem and an incomplete, but useful, solver that was applied to infer pre/post procedure specs without knowing the calling context at a much larger scale (> 1M LOC).

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

  • Heap-Hop (Paris): Smallfoot extension for message-passing programs.

  • Hip (Singapore)

  • jStar (London/Cambridge): SL-based verifier for Java programs.

  • SmallfootRG (Cambridge): Smallfoot extension for fine-grained concurrent algorithms.

  • Verifast (Leuven): verifier for Java and C.

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.

  • CAVE (Cambridge/Kaiserslautern): verifies linearizability of fine-grained concurrent algorithms (using a variety of techniques in addition to SL).

  • Space Invader (London)

  • SLAyer (Cambridge): MS Windows device drivers.

  • THOR (Pittsburgh): generates integer programs abstracting the SL proof.

  • Xisa (Colorado/Paris): supports user-defined inductive data structures.

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:

  • A local shape analysis based on separation logic. D Distefano, P O'Hearn and H Yang. In TACAS 2006, LNCS 3920, pp287-302.
    This paper introduces the domain of singly linked non-empty list segments.

  • Scalable Shape Analysis for Systems Code. H Yang, O Lee, J Berdine, C Calcagno, B Cook, D Distefano and P O'Hearn. CAV 2008.
    This paper shows a carefully designed join operation for scaling shape analysis to entire Microsoft and Linux device drivers of up to 10K LOC.

  • Compositional Shape Analysis by means of Bi-Abduction. C Calcagno, D Distefano, PW O'Hearn and H Yang. POPL 2009.
    This paper extends the frame inference question to a bi-abductive inference question: Given $P$ and $Q$ find $F$ (the frame) and $A$ (the anti-frame) such that $P * A \vdash Q * F$. The paper describes an ordering on the solutions to this problem and an incomplete, but useful, solver that was applied to infer pre/post procedure specs without knowing the calling context at a much larger scale (> 1M LOC).

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