## About S2S

S2S is an efficient and automatic decision procedure for problems in separation logic extended with string constraints.
It can be used to prove the validity of both entailment and satisfiability
of separation/string logic formulas.

## Features

entailment and satisfiability problems of separation logic with

inductive predicates

integer arithmetic

satisfiability problems of string logic with

concatenation

regular memberships

length constraints

## Download

0.3.3 (March 2019 - tested on Ubuntu 14.04, Ubuntu 16.04 and Ubuntu 18.04).

License: academic use only.

Warranty information:

This version was dedicated to SL-COMP 2019. It is not an official release.
SL-COMP 2019 benchmarks in S2S grammar could be downloaded here.
The tool may contain bugs; use it with your own risks: "see it, send it, sorted".
New features are actively developed and updated.
## Input Grammar (Updating)

```
program ::= (cell_definition | inductive_definition | command )*
cell_definition ::=
'ddata' cell_name '{' (type ID;)* '}' '.'
inductive_definition ::=
'pred' inductive_name'<'(variable:type)+ '>' '==' formula ('or' formula)* '.'
command ::=
| 'checksat' formula.
| 'checkent' formula '|-' formula '.'
formula ::=
| heap_formula '&' pure_formula
| '(' 'exists' variable '.' formula ')'
heap_formula ::=
| 'emp'
| variable '::' cell_name '<' expression* '>'
| inductive_name '(' expression+ ')'
| heap_formula '*' heap_formula
pure_formula ::=
| 'true'
| 'false'
| exp '=' exp
| exp '!=' exp
| exp '>' exp
| exp '>=' exp
| exp '<' exp
| exp '<=' exp
| '!' pure_formula
| pure_formula '&' pure_formula
| pure_formula '|' pure_formula
| '(' 'exists' variable '.' pure_formula ')'
| '(' 'forall' variable '.' pure_formula ')'
exp ::=
| integer
| variable
| char | word
| null
| '-' exp
| expr '+' exp
| exp '-' exp
| integer '\*' exp
type ::=
| 'int'
| cell_name
variable ::= ID
cell_name ::= ID
inductive_name ::= ID
ID ::= [a-zA-Z_][a-zA-Z0-9_]*
integer ::= [0-9]+
```

### An example

```
ddata RefSll_t {
RefSll_t next;
int data;
}.
pred lsls< in:RefSll_t,dt1:int,len1:int,out:RefSll_t,dt2:int,len2:int > ==
emp & in = out & dt1 = dt2 & len1 = len2
or (exists u,dt3,len3: in::RefSll_t * lsls(u,dt3,len3,out,dt2,len2) & dt1 < dt3+0 & len1 = len3+1).
checksat lsls(u_emp,d1,n1,z_emp,d2,n2) * z_emp::RefSll_t * lsls(y_emp,d3,n3,w_emp,d4,n4) & d1 != d2 & n3 = n4+3.
```

## Developers

Quang Loc Le

## Contact

lequangloc@gmail.com for
bug report and discussion.

## Acknowledgments

Mihaela Sighireanu, the Chair, and the contributors of SL-COMP. At the early stage of the development, S2S was tested mainly by the bechmarks of SL-COMP 2018.