SPEN
Solver for Separation Logic Entailments

Contents

Introduction

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)
The definition of the SMTLIB2 theories used as input of SPEN is available in files slrd-theory.smt (for the fragment in [1]) slrdi-theory.smt (for the fragment in [2]).

Output

Examples

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

Credits

Download

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

For installing SPEN you need:

References

[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