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 2 (tested with version 2.7)

2. License, Download, Instalation

License GNU GPL v3 or any later, see 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)
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:

Single file input format benchmarks

A set of benchmarks prepared for SMTCOMP 2014, separation logic competition can be downloaded here. To run the slide on these benchmarks, use:

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,
Tomas Vojnar
Radu Iosif

Last changes: 16th June 2014