World's Most Prestigious Award in Computer Science to Weizmann Institute's Prof. Amir Pnueli

 

 

Pnueli develops sophisticated methods for verifying the correctness and reliability of computer systems, including software and hardware. These increasingly complex 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 sometimes catastrophic consequences.

One way to prevent such disasters is to test the computer's response to a range of simulated situations. However, sophisticated as this method may be, there is always a risk that the check-up may overlook one scenario -- which may happen to be the one that can trigger a meltdown .

A far more reliable approach has been developed by Pnueli. He uses a mathematical language to describe the desired specifications of a program and -- before the system is even built -- applies mathematical proofs to confirm beyond a shadow of a doubt that the program complies with the most stringent safety standards. This prize-winning method is particularly suitable for programs that control physical facilities, such as those that govern the flight of an aircraft.

The A.M. Turing Award is named after Alan M. Turing (1912-1954), the Scottish mathematician considered to be among the fathers of modern computer science. He was on the British team that deciphered the German army s Enigma codes during World War II.

The Award is granted annually by the Association for Computing Machinery for major and lasting contributions to the computing community. It will be presented to Pnueli in March 1997 in San Jose, California, at the scientific meeting marking the 50th anniversary of the association, the largest international scientific and educational computer society.

 

In his research, Pnueli, a member of the Weizmann Institute's Applied Mathematics and Computer Science Department, relies on temporal logic, a mathematical language that incorporates the element of time into mathematical reasoning. For example, it can distinguish between things that are true at all times and properties that may be true in one instant but false in another.

Pnueli's innovative approach, first published in 1977, introduced temporal logic into computer science as the appropriate language for specifying and verifying reactive programs. By now, this use of temporal logic has been widely accepted and has led to the emergence of the new and dynamic field of temporal specification and verification in computer science.

Verification techniques based on his work have in the past few years been used worldwide both as a research tool and in practical applications, particularly in large and complicated systems.

Pnueli is responsible for the introduction of a number of new concepts, computational models and verification methodologies that have been adopted by the entire scientific community dealing with system verification.

For example, he characterized the class of reactive systems as systems whose role is to maintain an ongoing interaction with their environment, rather than compute a final result. He argued that such systems are particularly difficult to program correctly, and showed that temporal logic is the right tool for their specification and verification. Today the notion of reactive systems has become a key concept in computer science and is the topic of numerous research papers and international conferences.

An important extension to the temporal methodology was Pnueli's development of real-time temporal logic, which makes possible the precise analysis of real-time systems whose reliability is dependent on their ability to react to external stimuli within particularly short time periods. This improvement stirred up a flurry of activity in the international scientific community.

Another concept recently developed by Pnueli is that of hybrid systems. For many years, it was common to distinguish between discrete components (such as a digital controller that decides on the opening and closing of valves) and continuous ones (such as the chemical and physical processes themselves).

A system that controls a production line in a large factory naturally includes both discrete and continuous components. Pnueli found a way to combine these components into the single mathematical model of hybrid systems which can be specified and verified by temporal technology.

Pnueli is personally involved in numerous research projects at various international institutions. He plays a key role in a major European Union project aimed at developing a foolproof design methodology for safety-critical systems. These are legally characterized as systems in which a single failure can cause the death of one or more persons.

Born in Nahalal, Israel, Pnueli received his Ph.D. at the Weizmann Institute and then conducted research at Stanford University in the U.S. He founded and headed the Department of Computer Science at Tel Aviv University before returning to the Weizmann Institute in 1980.