A.M. TURING CENTENARY CELEBRATION WEBCAST
  • go to Leonard M. Adleman's profile page
  • go to Joseph Sifakis's profile page
  • go to Alan Kay's profile page
  • go to Raj Reddy's profile page
  • go to Michael O. Rabin 's profile page
  • go to Charles W Bachman's profile page
  • go to Judea Pearl's profile page
  • go to Edgar F. Codd's profile page
  • go to Niklaus E. Wirth's profile page
  • go to Ole-Johan Dahl 's profile page
  • go to Donald E. Knuth's profile page
  • go to Silvio Micali's profile page
  • go to E. Allen Emerson's profile page
  • go to A. J. Perlis 's profile page
  • go to C. Antony R. Hoare 's profile page
  • go to Kenneth E. Iverson 's profile page
  • go to John L Hennessy's profile page
  • go to Richard Karp's profile page
  • go to Peter Naur's profile page
  • go to Adi Shamir's profile page
  • go to Maurice V. Wilkes's profile page
  • go to Yann LeCun's profile page
  • go to Richard W. Hamming's profile page
  • go to Stephen A Cook's profile page
A.M. TURING AWARD WINNERS BY...
Amir Pnueli

Amir Pnueli DL Author Profile link

United States – 1996
Short Annotated Bibliography
  1. Pnueli, A., “The Temporal Logic of Programs,” Proceedings of the 18th annual symposium on Foundations of Computer Science, pp. 46-57, 1977.This paper revolutionized the way computer programs are analyzed.  At the time, program verification focused on programs that receive inputs at the beginning of computation and produce output at the end (“transformational.”) In this seminal work Amir considers verification of programs, (later termed “reactive”) that interact with their environment and do not necessarily terminate, such as concurrent programs or operating systems. Linear Time Temporal Logic was proposed as a unifying approach to specify and verify both transformational and reactive systems. The paper also describes a model checking algorithm for finite-state programs.
  2. Harel, D., H. Lachover, A Pnueli, M. Politi, R. Sherman A. Shtull-Trauring, and M. Trakhtenbrot, “STATEMATE: a working environment for the development of complex reactive systems,” IEEE transactions on Software Engineering, Vol. 16, Num. 4, pp. 403-414, 1990.This paper introduced the first viable commercial-level tool for executable specifications, based on Harel's language of statecharts. It won the Best Paper Award in the 1988 ICSE conference, the Most Influential Paper Award ten years later at the same conference, and the 2007 ACM Software Systems Award.
  3. Pnueli, A., “The Temporal Semantics of Concurrent Programs,” Theoretical Computer Science, Vol. 13, Num. 1, pp. 45-60, 1981.This paper introduces a model of (strongly) fair concurrent programs using shared variables, describes how to attain a temporal formula that describes all fair executions of the system, and how to obtain a proof that the system satisfies its temporal logic specifications.
  4. Lichtenstein, O. and A. Pnueli, “Checking that Finite State Concurrent Programs satisfy their Linear Specification,” Proceeding of the 12th ACM Symposium on Principles of Programming Languages, 1985.This paper introduces an efficient model checking algorithm to verify temporal properties over finite-state concurrent programs. The algorithm yields either a proof of correctness or a counter-example. The run-time of the algorithm is linear in the size of the system and exponential in the size of the formula. Various notions of fairness are considered.
  5. Gabby, D., A. Pnueli, S. Shelah and J. Stavi, “On the Temporal Analysis of Fairness,” Proceeding of the 7th ACM Symposium on Principles of Programming Languages, 1980.This paper, known as “GPSS,” introduces a temporal logic with a single temporal operator (a variant of the commonly used “Until”), shows it to be expressively complete and presents a deductive system for the logic. One of the main implications of this paper is that temporal logic that reasons only about the future is as expressive as one that reasons about both the future and the past.
  6. Pnuei A. and R. Rosner, “On the Synthesis of a Reactive Module,” Proceeding of the 16th ACM Symposium on Principles of Programming Languages, 1989.This paper studies the problem of synthesizing a reactive module within a synchronous open environment. The synthesis of a reactive module from its linear temporal logic specifications is shown equivalent to the validity problem of a corresponding quantified branching-time implementability formula over all tree models. A synthesis algorithm whose complexity is double exponential in the length of the given specification is provided for the finite state case.
  7. Ben-Ari, M., A. Pnueli and Z. Manna, “The Temporal Logic of Branching Time,” Acta Informatica, Vol. 20, Num. 3, pp. 207-226, 1983.The paper introduces UB – a branching time temporal logic (in today’s terms, CTL without the Until operator), provides the first practical model checking algorithm for the logic as well as a simple axiomatization which is shown to be complete.
  8. Pnueli,A., “Applications of Temporal Logic to the Specification and Verification of Reactive Systems: A survey of Current Trends,” in “Current Trends in Concurrency,” Lecture Notes in Computer Science, Vol. 224, pp. 510-584, 1986.This survey paper presents an overview of Amir's work, with several collaborators, on the applications of temporal logic to the specification and verification of reactive systems.  It first presents a formal computational model and shows how it abstracts other models (including CSP and Petri Nets).  It then presents temporal logic with several extensions.  Finally, a global and a preliminary approach for modular proof systems for verifying temporal properties of reactive systems are presented.  The paper contains numerous examples.
  9. Maler, O., A. Pnueli and J. Sifakis, “On the Synthesis of Discrete Controllers for Timed Systems,” Proceedings of STACS, Lecture Notes in Computer Science, Vol. 900, pp. 229-342, 1995.This paper extends the notion of synthesis to timed systems using the model of a Timed Game Automaton, which captures situations where an agent needs to take decisions in the presence of the uncertainty of the environment.  A typical situation would be a decision of whether to walk or wait for the next bus, given some bounds on its inter-arrival times. The problem has been solved by defining a controllable predecessors operator and showing that winning states and strategies can be computed as a fixpoint in the spirit of dynamic programming.
  10. Lichtenstein, O., A. Pnueli and L. D. Zuck, “The Glory of the Past,” Logics of Programs, Lecture Notes in Computer Science Vol. 193, pp. 196-218, 1985.While GPSS showed that bounded past operators do not add to the expressive power of temporal logic, this paper re-introduces the bounded past operators into the logic, extends model checking to handle them, and studies the advantages offered by them including clear classification of temporal properties as well as sound and complete model checking technique for showing that finite-state probabilistic programs satisfy their temporal specification with probability 1.