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 model,
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.
Songbird has been developed in OCaml and evaluated with
benchmarks of handcrafted entailments as well as
entailments from
SL-COMP,
a competition for Separation Logic provers.
The experiment result is encouraging as
it shows the usefulness and essentials of the
* mutual explicit induction *
proof technique in proving SL entailments.

- Try out Songbird online.
- Download the Songbird prover.
- Checkout the detailed experiment results.

- The benchmark slrd_entl (SL-COMP) with valid entailments. (Full benchmark slrd_entl can be accessed here)
- The benchmark slrd_ind of hand-crafted entailments.

- Dr. Khoo Siau Cheng - (Associate Profesor - National University of Singapore).
- Dr. Chin Wei Ngan - (Associate Profesor - National University of Singapore).
- Dr. Le Ton Chanh - (Research Fellow - National University of Singapore).
- Ta Quang Trung - (PhD Candidate - National University of Singapore).

Last updated: