[talks] David Naumann--Colloquium Speaker, Wednesday, October 18, 2009

[Michele J. Brown]

Title: Smart Assertions for Dumb Provers
David Naumann, Stevens Institute of Technology
4:30PM- Small Auditorium CS105
Host: Andrew Appel

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.

Joint work with Anindya Banerjee, Mike Barnett, and Stan Rosenberg