Verifying correctness and reliability of computer hardware and software

 

Prof. Amir Pnueli developed sophisticated methods for verifying the correctness and reliability of computer hardware and software. He used a mathematical language called temporal logic, which makes it possible to formulate and prove theorems that contain statements relating to time.

 

 

Pnueli’s research is being implemented in control systems of nuclear reactors and space missile launchers. It is also being considered for use in creating “smart roads” equipped with sensors for preventing traffic accidents.