Welcome to our home page!

Songbird is an automated theorem prover for Separation Logic entailments. At its core, Songbird employs mathematical induction to prove entailments involving user-defined inductive heap predicates. In addition, Songbird is also equipped with powerful proof techniques to assist in proving the entailments. These include a mutual induction proof system and a lemma synthesis framework. More details can be found out in our sub-projects: