Some user-facing aspects of the system are described in the following papers.
- Automated Verification of Shape, Size and Bag Properties via User-Defined Predicates in Separation Logic (SCP 2012)
- Structured Specifications for Better Verification of Heap-Manipulating Programs (FM 2011)
- Immutable specifications for more concise and precise verification (OOPSLA 2011)
- Translation and optimization for a core calculus with exceptions (PEPM 2009)
- Enhancing Program Verification with Lemmas (CAV 2008)
- Enhancing modular OO verification with separation logic (POPL 2008)
- Multiple Pre/Post Specifications for Heap-Manipulating Methods. HASE 2007