12-16

Smart Assertions for Dumb Provers

Assertions are widely used for runtime checking of software correctness, and increasingly used for compile time checking of simple properties like array index bounds. Structural integrity of pointer based data structures and design patterns often involves recursively defined properties which are costly to check at runtime and which appear to be unsuited to static checking using fully automated theorem provers. Remarkably, judicious use of ghost state lets programmers express recursive properties in pure first order logic and successfully use fast provers based on SAT solving. In this talk I will introduce the technique in elementary terms, for programmers, who may find it immediately useful in testing. I will also outline research questions about how to use the technique in frame conditions, in refactoring, in foundational proofs, in refinement types, in terms of aspects, and in checking information flow properties.