6th Milton Bender Lecture

On March 5th, 1998, Professor Amir Pnueli gave the 6th Milton Bender Lecture in AIT.

The Lecture was entitled "Practical Formal Verification: How Close are We?". Material of the lecture can be accessed as abstract, slides or computerized video.

To offer a wider audiance the opportunity to listen the Lecture, it was made available on the Internet. See the details of the technical setting for broadcasting.

Prof. Amir Pnueli, a Science Mathematician cum Computer Scientist of the Weizmann Institute of Science, Israel, he recently received the World's most prestigious Turing Award in Computer Science dubbed the "Nobel Prize in Computer Science". The award was made to Prof. Pnueli on the occasion of the 50th Anniversary Scientific Meeting of the International Scientific and Educational Computer Society.

Prof. Pnueli developed sophisticated methods for verifying the correctness and the reliability of computer systems, including software and hardware. These innovative systems control crucial aspects of contemporary life, such as the operation of nuclear power stations, missile launching, aircraft navigation, functioning of medical equipment and communications. A fault in these vital computer systems can have grave and even catastrophic consequences. Unlike the conventional way for the prevention of such disasters in testing the computer's response to a range of simulated situations, the prize-winning method of Prof. Pnueli uses a mathematical language to describe the desired specifications of a program, even before the system is built. It applies mathematical proofs to confirm beyond a shadow of a doubt that the program complies with the most stringent safety standards. Thus the Prof. Pnueli's Method is well suited for programs that control physical facilities, such as those that govern the flight of an aircraft. His innovative approach first published in 1977 introduce temporal login into computer science as the appropriate language for specifying and verifying reactive programs. This widely accepted use of temporal logic has led to the emergence of the most vibrant and new dynamic field of temporal specification and verification in computer science.

Born in Nahalal, Israel, Prof. Pnueli received his Ph.D at the Weizmann Institute in Israel and conducted research at Stanford University in U.S.A. He is also the founder of the Department of Computer Science at Tel Aviv University.