SPEN
Solver for Separation Logic Entailments

• Introduction
• Examples
• Credits
• Download
• References

SPEN (SeParation logic ENtailment) is a solver for checking validity of entailments between formulas in fragments of Separation Logic with inductive definitions.

The logic fragments have been defined in [1] and [2]. They mainly contains existentially quantified Separation Logic formulas with spatial atoms represeting complex data structures defined using inductive definitions. The inductive definitions may specify, for example, doubly linked lists, nested linked lists, fixed depth skip lists, binary search trees, AVL, red-black trees, etc.

Input

SPEN takes as the input a file in the SMTLIB2 format, which includes the recursive definitions used and the entailment problem A => B written as:

(assert A)
(assert not(B))
(check-sat)

Output

• If the checked entailment is valid, the tool outputs unsat (corresponding to the fact that the negation of the entailment problem is unsatisfiable).
• If the checked entailment is invalid, SPEN outputs sat and prints a diagnosis in the form of the atom of B not covered by A.

SPEN has been applied on the following benchmarks suites (included in the distribution):

• SLCOMP'14 divisions sll0a_sat, sll0a_entl, FDB_entl, which include, for example, verification conditions from programs with:
  • nested singly linked lists: nll-vc01
  • doubly linked lists: dll-vc01
  • nested cyclic lists: nlcl-vc01
  • skip lists of level 3: skl3-vc01
• Verification conditions from iterative programs with inductively defined data structures:
  • sorted linked lists: sls-insert-vc01
  • binary search trees: bst-insert-vc01
  • AVL: avl-insert-vc01
  • red black trees: rbt-insert-vc01

• Constantin Enea
• Ondrej Lengal
• Mihaela Sighireanu
• Tomas Vojnar
• Zhilin Wu

You can download the SPEN last version from its in the github repository.

For installing SPEN you need:

• Bison >= 2.7, Flex >= 2.4
• Cmake >= 2.8.2
• GCC >= 4.8.0
• Minisat incremental version
• VATA library
• SMTLIB2 parser.
• Z3 solver.

[1] C. Enea, O. Lengal, M. Sighireanu and T. Vojnar. Compositional Entailment Checking for a Fragment of Separation Logic. Technical Report FIT-TR-2014-01, FIT BUT, 2014.

[2] C. Enea, M. Sighireanu and Z. Wu. Automating Program Proofs Based on Separation Logic with Inductive Definitions. submitted 2015.

Last updated: Wed Feb 4 22:21:09 CET 2015