What is Songbird?

Songbird is an automated inductive theorem prover for Separation Logic. It employs mathematical induction to prove entailments involving general inductive heap predicates. In particular, the proof technique of Songbird is called mutual explicit induction, which inherits advantages of both explicit induction and implicit induction. The induction principle is designed based on a well-founded relation on Separation Logic models, and has been directly implemented as inference rules of Songbird. In addition, entailments derived during proof search can be used as hypotheses to prove other derived entailments, and vice versa, thanks to flexibility of the proposed well-founded relation.

How good is Songbird?

We have implemented Songbird in OCaml and evaluated with two entailment benchmarks from SL-COMP 2014, a competition for Separation Logic provers, as well as a hand-crafted benchmark. The experimental result is encouraging as it shows the usefulness and essentials of the mutual explicit induction proof technique in proving separation logic entailments.

• Summary of the first experiment on the existing SL-COMP benchmarks:
• Pair-wise comparison between Songbird and other provers on the SL-COMP benchmarks:
• Summary of the second experiment on the handcrafted benchmark:
• View details of all the two experiments

Download and usage

Download links for the Songbird prover and the benchmarks are presented below:

• Download the Songbird prover
• Download the benchmarks

In this release, the binary of Songbird is named songbirdand is supposed to run under a Linux environment, preferably Ubuntu-based operating systems. Songbird is shipped with a binary file z3 of the Z3 SMT solver. Given that both the two binary files songbird and z3 are placed at the current working directory ./, and test.sb is an input file containing a goal entailment then the command to run Songbird is:

        
./songbird test.sb
        
      

Sample input and output

A sample input of the Songbird 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;
};

// Several definitions of inductive heap predicates modelling the linked list

pred ls(x,y) := x=y
    \/ (exists u. x->node{u} * ls(u,y));

pred ls_even(x,y) := exists u. x->node{u} * ls_odd(u,y);

pred ls_odd(x,y) := x->node{y}
    \/ (exists u. x->node{u} * ls_even(u,y));

pred ls_all(x,y) := ls_even(x,y) \/ ls_odd(x,y);

// The goal entailment

checkentail ls_all(x,y) * ls_odd(y,z) |- ls(x,z);
        
      

Output when running: ./songbird test.sb

        
user@linux ~ $ ./songbird test.sb

[+] CheckEntail ls_all(x,y) * ls_odd(y,z) |- ls(x,z)

 ==> Time: 0.0449190139771 (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)*