Songbird: an inductive theorem prover for Separation Logic

Introduction

Note: Songbird has moved to its new nest. Please visit its new homepage to find out more details


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.

Download Songbird prover and benchmarks

Please find the details in the new homepage of Songbird

People


Last updated: