Amir Pnueli

Estrin Family Professor of Computer Science


My field of research concerns the application of formal (mathematical) methods to the specification, verification, systematic development, and automatic synthesis of reactive, real-time, and hybrid computerized systems.

The mission of formal methods is to guarantee, using mathematical and logical techniques, that constructed systems (and programs) are correct, reliable, and absolutely error-free. My work so far has concentrated on the use of temporal logic, and its appropriate extensions for real time and hybrid systems, as a convenient specification language, and the development of deductive and algorithmic (model checking) techniques for verifying that a given system satisfies its specification.

My current activities in this general area involve the application and enhancements of deductive verification methods to hardware designs such as the out-of-order execution component of modern micro-process chips, tools and methods for verifying the correctness of translators from a high-level specification into a running code, the development of methods for symbolic model checking of parameterized systems, and general techniques for using abstraction and composition as part of the verification process, enabling the handling of very large designs and systems.


Recent Publications


Personal Web Page