Personal tools
You are here: Home Events Milner Lectures 2008 Milner Lecture

2008 Milner Lecture

Software Model Checking


Professor Rajeev Alur, University of Pennsylvania


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.

Document Actions