Skip to main content


HVC 2010
Haifa Verification Conference 2010

October 5-7, 2010
Organized by IBM R&D Labs in Israel

image: IBM and Haifa


Invited Speakers and Special Sessions

Special session dedicated to the memory of Amir Pnueli:

Professor Amir Pnueli was one of the pioneers in the specification and verification of computer systems. He received the 1996 ACM Turing Award, the highest distinction that can be given to a computer scientist, for his seminal work introducing temporal logic into computing science and for outstanding contributions to program and system verification.

Amir Pnueli was born in Nahalal, Israel in 1941. He received his BSc in mathematics from the Technion in Haifa, and his Ph.D. in applied mathematics from the Weizmann Institute of Science in 1967. His PhD thesis focused on the "Calculation of Tides in the Ocean". He then switched from mathematics to computer science during his post doctoral fellowship at Stanford University and the IBM T.J. Watson Research Center.

Prof. Pnueli returned to the Department of Applied Mathematics of the Weizmann Institute to a position of a Senior Researcher after his post doc in the US. In 1973, he moved to Tel-Aviv University, where he founded the Department of Computer Science and was its first chairman. In 1981, Prof. Pnueli returned to the Weizmann Institute as a Professor of Computer Science. From 1999, he also served as a professor in the Department of Computer Science at NYU.

Prof. Pnueli believed in applying theory to practice. He was also one of the pioneers of the Israeli hi-tech industry. He co-founded two software companies, one of which (i-Logix) became part of IBM in 2008.

For his outstanding contribution to the Israeli academy and Industry, Prof. Pnueli was awarded the 2000 Israel Prize.

He was a foreign associate of the US National Academy of Engineering, a foreign member of the Academia Europaea, and a member of the Israel Academy of Sciences and Humanities. He received numerous other professional accolades.

Amir Pnueli passed away on November 2, 2009. He is survived by his wife Ariela, two daughters, a son, and four grandchildren.

Personal remarks - David Harel, The Weizmann Institute of Science
Temporal logic and model checking - Orna Grumberg, Technion
Parameterized system verification - Lenore Zuck, University of Illinois
Synthesis of temporal logic - Roderick Bloem, Graz University of Technology

Contact Information

Proceedings Publication

Springer Lecture Notes in Computer Science