Amir Pnueli

Amir Pnueli was an Israeli computer scientist who in 1977 introduced temporal logic as a formal tool for specifying and reasoning about the ongoing behavior of concurrent and reactive computer programs, systems that run continuously and respond to events rather than simply computing an output and stopping. This work became foundational to the later development of model checking and automated verification. Pnueli won the Turing Award in 1996.