Department of Computer Science

Amir Pnueli

Date: April 14, 2005

Time: 3:40PM

Location: 1148 Gerdin Building

Title: Taming the Infinite: Verification of Infinite-State Systems

Abstract: Computers are helping us manage and control more extended areas of our life. The main obstacle to trusting to them more sensitive tasks is not speed or reliability of the hardware but rather the question of trustworthiness of the software -- the programs that drive and control such safety-critical applications

In this talk we will survey advances in the most promising approach to absolute reliability of software -- formal verification. At a first glance this problem seems hopeless since even simple systems possess infinitely many states and even higher infinity of possible behaviors, and formal verification calls for exhaustive exploration of this infinite state space.

We will start by describing the effective methods developed for the handling of finite-state systems, which proved most useful for verification of hardware designs. Then, we will consider various methods, relying on different notions of abstraction, by which an infinite-state system can be reduced to a finite-state one and thus yield to effective analysis.

This general approach will be illustrated by several success stories, including the case of verification of device drivers at Microsoft, and successful analysis of the avionic software of the Airbus plane.

About the Speaker: Amir Pnueli received his Ph.D. degree in Applied Mathematics at the Weizmann Institute of Science, Rehovot, Israel where, since 1981, he has been a Professor of Computer Science, and since 1998 head of the "Minerva Center for Verification of Reactive Systems." Since 1999 he is a professor of Computer Science at NYU. Prof. Pnueli is the 1996 recipient of the ACM Turing award "For his seminal work introducing temporal logic into computing science and for outstanding contributions to program and system verification." He is a member of the National Academy of Engineering, the Israeli Academy of Arts and Sciences, and the 2000 recipient of the Israel prize in the category of exact sciences. He received honorary doctorates from the Universities of Uppsala, Joseph Fourier (Grenoble, France), and University of Oldenburg, Germany. Prof. Pnueli is mainly known for the introduction of temporal logic into Computer Science and his work on the application of temporal logic to the specification and verification of reactive systems. Together with David Harel, Pnueli worked on the semantics and implementation of Statecharts, a visual language for the specification, modeling, and prototyping of reactive systems, applied to avionics, transport, and electronic hardware systems. His current research interests involve synthesis of reactive modules, automatic verification of multi-process systems, and specification methods that combine transition systems with temporal logic.