SLIDE - Separation Logic with Inductive Definitions

Automata-based entailment checking for Separation Logic with Inductive Definitions

SLIDE is a prototype tool for checking entailment in Separation Logic with user-provided inductive definitions of recursive data structures (lists, trees, and beyond)

Basic features:

Sound and complete for local data structures (doubly-linked lists, trees with parent pointers, etc.)
Sound for non-local data structures (trees with linked leaves, skip-lists, etc. )
Built on top of the VATA tree automata library.

Related Publications:

R. Iosif, A. Rogalewicz, T. Vojnar: Deciding Entailments in Inductive Separation Logic with Tree Automata. arXiv:1402.2127 [link]
R. Iosif, A. Rogalewicz, J. Šimáček: The Tree Width of Separation Logic with Recursive Definitions, CADE-24. [link]

1. Requirements

VATA tree automata library.
Python 3

2. License, Download, Instalation

License GNU GPL v3 or any later, see http://www.gnu.org/licenses/gpl.html for more details.

Download SLIDE
Unzip the file and enter directory slide.
Open the file settings.py and set variable VATA_path to the vata executable (usually located in libvata/build/cli/).

3. Examples and running the tool

Basic set

The basic set of examples can be downloaded here. This file contains all the examples mentioned in the experimental section of the paper [1] . The set of examples contains following files:

File name	Recursive definition
DLL.pred	DLL(p1,nil,p2,nil)
DLL-rev.pred	DLL_rev(p1,nil,p2,nil)
DLL-mid.pred	DLL_mid(p1,nil,p2,nil)
node+DLL-rev+DLL.pred	\ex. x,n,b. x-> (n,b) * DLL_rev(p1,nil,b,x) * DLL(n,x,p2,nil)
node+node+DLL.pred	\ex. y,a. p1-> (y,nil) * y->(a,p1) * DLL(a,y,p2,\nil)
dll-rev+dll.pred	\ex. x,b. DLL_rev(x,b,p2,nil) * DLL(p1,nil,b,x)
DLL0+.pred	DLL0+(p1,nil,p2,nil)
TREE-pp.pred	TREE_pp(p1,nil)
TREE-pp-rev.pred	TREE_pp^rev(p1,nil)
TLL-pp.pred	TLL_pp(p1,nil,ml,mr)
TLL-pp-rev.pred	TLL_pp^rev(p1,nil,ml,mr)
node+TLL-pp.pred	\ex. l,r,z. p1->(l,r,nil,nil) * TLL (l,p1,ml,z)* TLL(r,p1,z,mr)

To run the tool, one of the following two ways may be used:

$ path/to/slide/entailment.py file_with_pred1 file_with_pred2
$ python path/to/slide/entailment.py file_with_pred1 file_with_pred2

Benchmarks in SLD format (SLIDE Single file input format)

A set of benchmarks prepared for SL-COMP'2014 in SLD format can be downloaded here.
A complete benchmark from SL-COMP'2018 translated into the SLD format can be downloaded here. (Not all benchmarks can be solved by SLIDE.)
To run the slide on these benchmarks, use: $ path/to/slide/slide-wrapper.sh file.sld

Cyclists benchmarks

A set of examples taken from CYCLIST framework rewritten into the SLIDE input format can be downloaded HERE To run the tool on these examples use:

$ path/to/slide/entailment.py 1.defs 2.defs

Adam Rogalewicz, rogalew@fit.vutbr.cz
Michal Cyprian
Tomas Vojnar
Radu Iosif

Last changes: 12th July 2018