Amir Pnueli

Pioneer of temporal logic in computing science, 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 introduced had extraordinary influence and proved to be of lasting value.

Pnueli's work was characterized as the most important contribution to program verification in the last twenty years, and it set the agenda for research and practice in the area.