Weizmann Institute of Science (1996)
Citation
"For seminal work introducing temporal logic into computing science and for outstanding contributions to program and system verification."

Amir Pnueli made a major breakthrough in the verification and certification of concurrent and reactive systems with his landmark 1977 paper "The Temporal Logic of Programs"(1) which was a crucial turning point in the progress of formal methods for such systems. This paper triggered a fundamental paradigm shift in reasoning about the dynamic behavior of systems; the techniques it introduces have had extraordinary influence and proven to be of lasting value. His work has been characterized as the most important contribution to program verification in the last twenty years and it has set the agenda for research and practice in the area.

Pnueli's work on temporal logic has been seminal. First, he focused on the ongoing behavior of programs rather than just their input/output behavior thereby introducing a powerful formalism for reasoning about programs. Second, by using temporal logic he made it possible to easily specify qualitative progress properties of concurrent programs without cumbersome timing details. Third, he recognized the value of carefully-chosen dedicated operators to deal with the temporal ordering of events and thereby establish a framework for reasoning about and mechanical verification of concurrent programs.

Beyond his pure scientific achievements, Amir Pnueli, a Professor of Computer Science at the Weizmann Institute of Science in Israel, is also keenly aware of the problems of putting computer science methods into practice and has been instrumental in founding two Israeli software firms. His work has influenced a large number of diverse industrial applications such as the process control of chemical plants, rule languages in active database systems, and the detection of complex race conditions in cache coherence protocols of computer architectures. By introducing temporal logic to computer science, Amir Pnueli has made a significant and lasting contribution which has been instrumental in shaping the study of concurrent systems.

(1) Proc. 18th IEEE Symp. Found. of Comp. Sci., 1977, pp. 46-57

Born in Nahalal, Israel, Pneuli received a Bachelor's degree in Mathematics at the Technion in Haifa, and PhD in applied mathematics from the Weizmann Institute of Science. His thesis was on the topic of "Calculation of Tides in the Ocean". He switched to computer science during a stint as a post-doctoral fellow at Stanford University. He returned to Israel as a researcher and after a sequence of academic appointments became a professor at the Weizmann Institute.

Pnueli has also founded two startup technology companies.

He is married and has 3 children and 1 grandchild.