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