What is SLS?

SLS is an lemma-synthesis-assisted 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 on-the-fly 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 sub-entailments, 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 three-step 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 SL-COMP, and also on a handcrafted benchmark. We have compared the performance of SLS with other state-of-the-art 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™ i7-6700 (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 state-of-the-art 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 64-bit Linux environment (preferably Ubuntu-based). 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 (pre-built for Ubuntu 64-bit 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 popl-18, and see the README file, located at popl-18/README. A convenient way to perform the experiment is to run the shell script popl-18/run_sls.sh.

Sample input and output

A sample input of the SLS prover is as below, where:

data, and pred 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,l-1));

// 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,l-1) * 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_5-2 |- (exists fv_11. fv_3->node{fv_4,fv_11} * dll(fv_1,fv_2,fv_11,fv_3,fv_5-1))
  - 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_5-2 |- (exists fv_11. fv_3->node{fv_4,fv_11} * dll(fv_1,fv_2,fv_11,fv_3,fv_5-1))
  - 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
       + Lemma-convert inferred: 2
       + Lemma-split inferred: 1
       + Lemma-combine inferred: 1
   - Number of lemmas used: 3
       + Lemma-convert used: 1
       + Lemma-split used: 1
       + Lemma-combine used: 1
   - Number of times using lemmas: 3
       + Lemma-convert using times: 1
       + Lemma-split using times: 1
       + Lemma-combine using times: 1
   - Runtime (in seconds) to infer all lemmas: 51.6794800758
       + Lemma-convert runtime: 20.9877829552
       + Lemma-split runtime: 17.6030759811
       + Lemma-combine 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 non-terminal program:

        
COMMENT         ::= '//' .*

INTEGER         ::=  [0-9]+

IDENTIFIER      ::=  [a-zA-Z_][a-zA-Z0-9_]*

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)*

SLS : Songbird + Lemma Synthesis

**A Separation Logic Prover which can Automatically Synthesize Inductive Lemmas On-the-fly**