Software Model Checking

Rajeev Alur

University of Pennsylvania

Abstract 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.

Biography

Rajeev Alur is Zisman Family Professor and Graduate Group Chair in the Department of Computer and Information Science at University of Pennsylvania. He obtained his bachelor's degree in computer science from Indian Institute of Technology at Kanpur in 1987, and PhD in computer science from Stanford University in 1991. Before joining Penn in 1997, he was with Computing Science Research Center in Bell Laboratories. His areas of research include formal modeling and analysis of reactive systems, hybrid systems, model checking, software verification, logics and automata, and design automation for embedded software. He is a Fellow of the ACM, and a Fellow of the IEEE.