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:
- 2018-07-13: Songbird participated in the Separation Logic Competition 2018 ( SL-COMP 2018) and is the best prover for 4 divisions: qf_shid_entl, qf_shidlia_entl, shid_entl, shidlia_entl. It can also solve 100% problems of other 2 divisions: qf_shls_entl, qf_shls_sat, although the runtime is slower than the best prover Asterix. There are totally 9 competitive divisions.
Automated Mutual Explicit Induction Proof in Separation Logic
The 21st International Symposium on Formal Methods (FM 2016)
Automated Mutual Induction Proof in Separation Logic
Submitted to Journal of Formal Aspects of Computing, August 2017 (under review)
Automated Lemma Synthesis in Symbolic-Heap Separation Logic
The 45th Symposium on Principles of Programming Languages (POPL 2018)
- Khoo Siau Cheng - Associcate Professor, School of Computing, National University of Singapore
- Chin Wei Ngan - Associcate Professor, School of Computing, National University of Singapore
- Ta Quang Trung - PhD candidate, School of Computing, National University of Singapore
- Le Ton Chanh - Research Fellow, School of Computing, Stevens Institute of Technology, USA
- Aishwarya Sivaraman - PhD candidate, University of California - Los Angeles, USA
- Nguyen Thanh Toan - PhD candidate, School of Computing, National University of Singapore