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 wellfounded 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 wellfounded relation.
How good is Songbird?
We have implemented Songbird in OCaml and evaluated with two entailment benchmarks from SLCOMP 2014, a competition for Separation Logic provers, as well as a handcrafted 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 SLCOMP benchmarks:
 Pairwise comparison between Songbird and other provers on the SLCOMP 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
songbird
and is supposed to
run under a Linux environment, preferably Ubuntubased 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
, 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;
};
// 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 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)*