What is SLS?
SLS is an lemmasynthesisassisted inductive theorem prover for separation logic entailments. It is developed on top of the inductive theorem prover Songbird, hence, the name SLS stands for Songbird + Lemma Synthesis. Essentially, SLS utilizes structural induction proof to deal with inductive heap predicates in the entailments. In addition, it is able to synthesize lemmas onthefly to assist in proving these entailments.
Why are lemmas needed?
Although structural induction is prominent for its application in reasoning recursive data structures, a sole use of this technique might not be sufficient to prove separation logic entailments. This is because the goal entailments might be too sophisticated to become good induction hypotheses.
SLS can automatically synthesize lemmas to assist in proving such sophisticated entailments. These lemmas are usually simple entailments, which can be easily proved by induction. Via lemma application, inductive heap predicates in the entailments can be reorganized, combined, or split to derive simpler subentailments, thus making the proof search of these (sophisticated) entailments more effective.
How are lemmas synthesized?
The supporting lemmas for a given goal entailment can be synthesized by a threestep recipe:
 Firstly, SLS identifies necessary lemma templates. They are simple entailments sharing similar heap (sub)structures with the goal entailment, with all variables freshly named.
 Secondly, SLS integrates unknown relations representing desired constraints about the templates' variables into the templates.
 Finally, SLS proves the lemma templates by induction to collect necessary assumption constraints about the unknown relations, then solves these constraints to discover actual definitions of the relations, thus discovers the desired lemmas.
How good SLS is?
We have implemented SLS in OCaml and evaluated it on existing entailments benchmarks, including benchmarks from the separation logic competition SLCOMP, and also on a handcrafted benchmark. We have compared the performance of SLS with other stateoftheart theorem provers in separation logic, including Slide, Sleek, Spen, Cyclist, and SMI (a version of Songbird supporting Mutual Induction proof). The experiments were conducted on a computer running Ubuntu 14.04 LTS, with CPU Intel® Core™ i76700 (3.4Ghz) and RAM 16GB. The participating provers were configured to prove each entailment within a timeout of 180 seconds.
The result shows that SLS can prove most of the valid entailments in the existing benchmarks, and also performed well in the handcrafted benchmark whose entailments are really sophisticated. Its result is also better than all the stateoftheart provers. Summary of the experiments are presented below, where SLD, SLK, SPN, and CCL respectively stand for Slide, Sleek, Spen, and Cyclist. The numbers which are highlighted in bold are the best results in each category. The spreadsheet containing all data of the two experiments is available here (redirecting to Google Sheets).
 Summary of the first experiment on the existing benchmarks:
 Summary of the second experiment on the handcrafted benchmark:
 View details of all the two experiments
Download and usage
In this release, the binary file of the prover
SLS is named sls
and is supposed to
run under a 64bit Linux environment (preferably Ubuntubased).
The SMT solver
Z3
is also required and its binary file z3
should be placed under the same directory with sls
.
Download links for the SLS prover and its benchmarks
are as below:
 Download the SLS prover
 Download the benchmarks
A sample command to run SLS is
./sls test.sb
,
given that both the two binary files
sls
and z3
are placed at
the current working directory ./
,
and test.sb
is an input file containing a goal
entailment.
POPL'18 Artifact Evaluation
We have prepared an experimental artifact for our accepted paper at POPL'18. This artifact contains a binary executable file of the prover SLS (prebuilt for Ubuntu 64bit environment), related entailment benchmarks and a shell script performing the experiment. The details are as follows:
 Download the packaged artifact (.zip file, about 9MB).
 Instruction: Please unzip the package into a folder,
named
popl18
, and see theREADME
file, located atpopl18/README
. A convenient way to perform the experiment is to run the shell scriptpopl18/run_sls.sh
.
Sample input and output
A sample input of the SLS prover is as below, where:

data
, andpred
are keywords corresponding to the declaration of singleton heap predicates and inductive heap predicates. 
node
is in identifier denoting the data sort. 
checkentail
is the keyword used to indicate the input entailment.
Sample input: test.sb
// This file name is: test.sb
// The definition of a simple data structure containing 2 fields,
// pointing to the previous and the next elements.
data node {
node next;
node prev;
};
// The definition of an inductive heap predicate modelling the doubly linked list
pred dll(hd,p,tl,n,l) := hd>node{n,p} & hd=tl & l=1
\/ (exists x. hd>node{x,p} * dll(x,hd,tl,n,l1));
// The definition of another inductive heap predicate modelling the doubly linked list,
// which is defined in a reversed direction
pred dll_rev(hd,p,tl,n,l) := hd>node{n,p} & hd=tl & l=1
\/ (exists x. dll_rev(hd,p,x,tl,l1) * tl>node{n,x});
// The goal entailment
checkentail dll_rev(x,y,u,v,n) * dll(v,u,z,t,200) & n>=100 
(exists u. dll(x,y,u,z,n+199) * z>node{t,u});
Output when running: ./sls test.sb
user@linux ~ $ ./sls test.sb
[+] CheckEntail dll(v,u,z,t,200) * dll_rev(x,y,u,v,n) & 100<=n  (exists u_1. z>node{t,u_1} * dll(x,y,u_1,z,n+199))
==> ALL LEMMAS SYNTHESIZED:
 Lemma lm_convert: infer_rhs_2: _dll_rev__entail__dll__1 (safe): dll_rev(hd_16,p_17,tl_18,n_19,l_20)  dll(hd_16,p_17,tl_18,n_19,l_20)
 Lemma lm_convert: infer_convert (reverse): _dll__entail__dll_rev__2 (safe): dll(hd_16,p_17,tl_18,n_19,l_20)  dll_rev(hd_16,p_17,tl_18,n_19,l_20)
 Lemma lm_split: infer_lhs: _dll__entail__dll_node__3 (safe): dll(fv_1,fv_2,fv_3,fv_4,fv_5) & 0<=fv_52  (exists fv_11. fv_3>node{fv_4,fv_11} * dll(fv_1,fv_2,fv_11,fv_3,fv_51))
 Lemma lm_combine: infer_lhs: _dll_dll__entail__dll__4 (safe): dll(fv_9,fv_8,fv_3,fv_4,fv_5) * dll(fv_6,fv_7,fv_8,fv_9,fv_10)  dll(fv_6,fv_7,fv_3,fv_4,fv_10+fv_5)
==> LEMMAS USED IN THE VALID PROOF:
 Lemma lm_combine: infer_lhs: _dll_dll__entail__dll__4 (safe): dll(fv_9,fv_8,fv_3,fv_4,fv_5) * dll(fv_6,fv_7,fv_8,fv_9,fv_10)  dll(fv_6,fv_7,fv_3,fv_4,fv_10+fv_5)
 Lemma lm_split: infer_lhs: _dll__entail__dll_node__3 (safe): dll(fv_1,fv_2,fv_3,fv_4,fv_5) & 0<=fv_52  (exists fv_11. fv_3>node{fv_4,fv_11} * dll(fv_1,fv_2,fv_11,fv_3,fv_51))
 Lemma lm_convert: infer_rhs_2: _dll_rev__entail__dll__1 (safe): dll_rev(hd_16,p_17,tl_18,n_19,l_20)  dll(hd_16,p_17,tl_18,n_19,l_20)
==> LEMMA SYNTHESIS STATS:
 Number of lemmas inferred: 4
+ Lemmaconvert inferred: 2
+ Lemmasplit inferred: 1
+ Lemmacombine inferred: 1
 Number of lemmas used: 3
+ Lemmaconvert used: 1
+ Lemmasplit used: 1
+ Lemmacombine used: 1
 Number of times using lemmas: 3
+ Lemmaconvert using times: 1
+ Lemmasplit using times: 1
+ Lemmacombine using times: 1
 Runtime (in seconds) to infer all lemmas: 51.6794800758
+ Lemmaconvert runtime: 20.9877829552
+ Lemmasplit runtime: 17.6030759811
+ Lemmacombine runtime: 13.0886211395
==> Time: 51.7247829437 (s)
==> Result: Valid
Input syntax
The syntax of an input file which contain entailments is represented
below, where the entry point is the nonterminal program
:
COMMENT ::= '//' .*
INTEGER ::= [09]+
IDENTIFIER ::= [azAZ_][azAZ09_]*
integer ::= INTEGER
variable ::= IDENTIFIER
field_name ::= IDENTIFIER
singleton_name ::= IDENTIFIER
inductive_name ::= IDENTIFIER
type ::=
 'int'
 singleton_name
int_expression ::=
 integer
 variable
 '' int_expression
 int_expression '+' int_expression
 int_expression '' int_expression
 integer '\*' int_expression
heap_expression ::=
 'null'
 variable
expression ::=
 int_expression
 heap_expression
pure_formula ::=
 'true'
 'false'
 int_expression '==' int_expression
 int_expression '!=' int_expression
 int_expression '>' int_expression
 int_expression '>=' int_expression
 int_expression '<' int_expression
 int_expression '<=' int_expression
 heap_expression '==' heap_expression
 heap_expression '!=' heap_expression
 '!' pure_formula
 pure_formula '&' pure_formula
 pure_formula '' pure_formula
 '(' 'exists' variable '.' pure_formula ')'
 '(' 'forall' variable '.' pure_formula ')'
heap_formula ::=
 'emp'
 variable '>' singleton_name '{' expression* '}'
 inductive_name '(' expression* ')'
 heap_formula * heap_formula
formula ::=
 pure_formula
 heap_formula
 heap_formula '&' pure_formula
 '(' 'exists' variable '.' formula ')'
singleton_defn ::=
 'data' singleton_name '{' (type field_name)* '}'
inductive_defn ::=
 'pred' indutive_name '(' variable* ')' ':=' formula ('\/' formula)* ';'
command ::= 'checkentail' formula '' formula ';'
comment ::= COMMENT
program ::= (singleton_defn  inductive_defn  command  comment)*