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:

Related Publications:

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

1. Requirements

  1. VATA tree automata library.
  2. Python 3

2. License, Download, Instalation

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


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 DLLrev(p1,nil,p2,nil)
DLL-mid.pred DLLmid(p1,nil,p2,nil)
node+DLL-rev+DLL.pred\ex. x,n,b. x-> (n,b) * DLLrev(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. DLLrev(x,b,p2,nil) * DLL(p1,nil,b,x)
DLL0+.pred DLL0+(p1,nil,p2,nil)
TREE-pp.predTREEpp(p1,nil)
TREE-pp-rev.predTREEpprev(p1,nil)
TLL-pp.predTLLpp(p1,nil,ml,mr)
TLL-pp-rev.pred TLLpprev(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:

Benchmarks in SLD format (SLIDE Single file input format)

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:


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

Last changes: 12th July 2018