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

[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. For pointer based data structures and design 
patterns, structural integrity conditions often involve 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, thereby enabling the use 
of fast provers based on SAT solving. In this talk I will introduce the 
technique and pose research questions about how to use the technique in 
frame conditions, in foundational proofs, in refinement types for higher 
order programs, in terms of aspects, and in checking information flow 
properties.

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