The 2008 Milner Lecture
Software Model Checking
Professor Rajeev Alur
Department of Computer and Information Science, University of Pennsylvania
5.15 p.m. on Wednesday, 23 July 2008
Lecture Theatre 1
Appleton Tower
Crichton Street, Edinburgh
and afterwards in the Forum for a reception
Building tools that can certify correctness of software systems with respect to their specifications, or reveal inconsistencies, remains a continuing challenge for computer science. In the first half of my talk, I will survey the progress in formal methods for specification and verification from early days of manual proofs of sorting programs using loop invariants to today's highly optimized and automated tools for discovering bugs in network protocols and device drivers. In the second half, I will describe some of the current research at Penn on software analysis. In particular, I will discuss the project CheckFence for checking consistency of concurrent data types on relaxed memory models, and ongoing efforts on a tool for certifying that a Java applet being downloaded on your cellphone won't leak confidential data from your addressbook.