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:
News
- 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.
Publications
-
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)
Contributors
- 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