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