Channels ▼

NYU Computer Science Professor Amir Pnueli, 68

NYU Department of Computer Science Professor Amir Pnueli died on November 2 of a brain hemorrhage. Professor Pnueli was an internationally recognized pioneer in the area of verification, the process of formally proving that systems, such as computer hardware and software, behave as intended by their designers.

Professor Pnueli served as Deputy Director for a team that recently received a five-year, $10 million grant from the National Science Foundation's Expeditions in Computing program to create revolutionary computational tools combining Model Checking and Abstract Interpretation.

Professor Pnueli was the recipient of the 1996 Association for Computing Machinery Alan M. Turing Award, the highest distinction that can be bestowed on a computer scientist. He was also the recipient of the Israel Prize, the state's highest honor. He was a foreign associate of the National Academy of Engineering, a foreign member of the Academia Europaea (Informatics section), and a member of the Israel Academy of Sciences and Humanities. He received honorary doctorate degrees from the University of Uppsala, Sweden, Joseph Fourier University, Grenoble, France, and the Carl von Ossietzky University of Oldenburg, Germany, as well as numerous other professional accolades. Amir Pnueli was born in Nahalal, Israel, on April 22, 1941. He received a B.Sc. degree in Mathematics from the Technion and a Ph.D. in Applied Mathematics from the Weizmann Institute of Science in 1967.

After a post-doctoral fellowship at Stanford University and the IBM T.J. Watson Research Center, he became a senior researcher at the Weizmann Institute. In 1973, Professor Pnueli founded the Department of Computer Science at Tel Aviv University and became its first chair. In 1981, he returned to the Weizmann Institute as Professor of Computer Science. In 1999, he joined the Courant Institute's Department of Computer Science at NYU, and in 2006 he was appointed to a Silver Professorship. He supervised more than 30 Ph.D. theses during his career in Israel and New York.

Professor Pnueli is particularly noted for introducing temporal logic, a formal technique for specifying and reasoning about the behavior of systems over time, to computer science. The 1996 Turing Award citation reads:
"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" 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 proved 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."

Professor Pnueli was an extremely prolific and deeply creative researcher with over 250 widely-cited publications and 4 books. In recent years, he worked on compiler and translation validation, the verification of concurrent systems, and fairness of infinite behaviors, as well as the application of mathematical and logical methods to the formal specification, compositional verification, systematic development, and automatic synthesis of reactive, real-time, discrete, continuous, and hybrid systems.

Professor Pnueli always advocated applying theory to practice and was instrumental in founding two Israeli software firms. His work has influenced a wide range of scientific disciplines, including process control, databases, biological modeling, and computer hardware design as well as the avionics, transport and electronic hardware industries. He shared the 2007 ACM Software System Award for Statemate, a software engineering tool that allows developers to formally specify the precise desired behavior of their programs. The citation for the award reads:
"Statemate was the first commercial computer-aided software engineering tool to successfully overcome the challenges of complex interactive, real time computer systems, known as reactive systems. The ideas reflected in Statemate underlie many of the most powerful and widely used tools in software and systems engineering today."

Related Reading

More Insights

Currently we allow the following HTML tags in comments:

Single tags

These tags can be used alone and don't need an ending tag.

<br> Defines a single line break

<hr> Defines a horizontal line

Matching tags

These require an ending tag - e.g. <i>italic text</i>

<a> Defines an anchor

<b> Defines bold text

<big> Defines big text

<blockquote> Defines a long quotation

<caption> Defines a table caption

<cite> Defines a citation

<code> Defines computer code text

<em> Defines emphasized text

<fieldset> Defines a border around elements in a form

<h1> This is heading 1

<h2> This is heading 2

<h3> This is heading 3

<h4> This is heading 4

<h5> This is heading 5

<h6> This is heading 6

<i> Defines italic text

<p> Defines a paragraph

<pre> Defines preformatted text

<q> Defines a short quotation

<samp> Defines sample computer code text

<small> Defines small text

<span> Defines a section in a document

<s> Defines strikethrough text

<strike> Defines strikethrough text

<strong> Defines strong text

<sub> Defines subscripted text

<sup> Defines superscripted text

<u> Defines underlined text

Dr. Dobb's encourages readers to engage in spirited, healthy debate, including taking us to task. However, Dr. Dobb's moderates all comments posted to our site, and reserves the right to modify or remove any content that it determines to be derogatory, offensive, inflammatory, vulgar, irrelevant/off-topic, racist or obvious marketing or spam. Dr. Dobb's further reserves the right to disable the profile of any commenter participating in said activities.

Disqus Tips To upload an avatar photo, first complete your Disqus profile. | View the list of supported HTML tags you can use to style comments. | Please read our commenting policy.