Improving Cee and ownership-based verification
Christoph Studer · Repository for Publications and Research Data (ETH Zurich) · 2009
Spec# is a verification system that allows programmers to statically verify object-oriented programs.Cee was developed as Jürg Billeter's master's thesis project to help programmers better understand Spec# verification failures.It generates counterexample programs that exhibit failing execution traces and are debuggable using the well-known debugger user interface.In this thesis, we enhanced Cee by contributing method side effect capturing, generation of runtime checks for frame conditions, and improved handling of method calls in contracts.Furthermore, our work enables integration of Cee with Visual Studio and other IDEs.As a separate effort, we designed and analyzed heap models for ownershipbased verification with the aim to improve verification performance.We evaluated these models within the Spec# system and consider none of them valid replacements for the current heap model.We discuss our findings in this report for future reference.