A.M. TURING CENTENARY CELEBRATION WEBCAST
  • go to John E Hopcroft's profile page
  • go to John Backus 's profile page
  • go to Alfred V Aho's profile page
  • go to Pat Hanrahan's profile page
  • go to Charles P. Thacker's profile page
  • go to Amir Pnueli's profile page
  • go to Stephen A Cook's profile page
  • go to Jim Gray 's profile page
  • go to Edwin Catmull's profile page
  • go to Joseph Sifakis's profile page
  • go to Kristen Nygaard 's profile page
  • go to Peter Naur's profile page
  • go to J. H. Wilkinson 's profile page
  • go to Butler W Lampson's profile page
  • go to Niklaus E. Wirth's profile page
  • go to Douglas Engelbart's profile page
  • go to Robert W. Floyd's profile page
  • go to David Patterson's profile page
  • go to Charles W Bachman's profile page
  • go to Prof. Martin Hellman's profile page
  • go to A. J. Perlis 's profile page
  • go to Leonard M. Adleman's profile page
  • go to Manuel Blum's profile page
  • go to E. Allen Emerson's profile page
A.M. TURING AWARD WINNERS BY...
E. Allen Emerson

PHOTOGRAPHS

E. Allen Emerson DL Author Profile link

United States – 2007
Short Annotated Bibliography
  1. Emerson, E. Allen, and Edmund M. Clarke, “Characterizing Correctness Properties of Parallel Programs Using Fixpoints,” International Colloquium on Automata, Languages and Programming, 1980.This paper, a precursor to the model checking work, describes a logic called CTF, similar to what we know today as the Computation Tree Logic CTL. The logic CTF and its modalities (basic temporal operators) are mapped to a fixpoint logic called FPF, which may be seen as an early modal µ-calculus. The fixpoint characterization would turn out crucial for CTL model checking algorithms.
  2. Clarke, Edmund M. and E. Allen Emerson, “Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic,” Logics of Programs, 1981.This paper first defines an algorithmic procedure to check temporal logic (specifically, CTL) specifications against labeled transition system models of programs, thus initiating the now-ubiquitous field of fully automated quality assurance. This paper introduces their use of the term "model checking." It also discusses the problem of synthesizing concurrent programs from CTL specifications.
  3. Emerson, E. Allen and Joseph Y. Halpern: “‘Sometimes’ and ‘Not Never’ revisited: On branching versus linear time temporal logic,” Journal of the ACM, Vol. 33, Num. 1,1986, pp. 151-178.This paper introduces the powerful computation tree logic CTL*, which combines features from CTL and the linear time temporal logic LTL, and is yet richer than the union of those two. This paper also analyzes the relationship between branching time logics (such as CTL) and linear time logics (such as LTL).
  4. Emerson, E. Allen and Chin-Laung Lei, “Efficient Model Checking in Fragments of the Propositional Mu-Calculus,” Logic in Computer Science, 1986.This paper, written by Emerson with his first graduate student, Chin-Laung Lei, describes an algorithm to detect certain types of cycles in directed graphs. This is important because model checking of LTL and CTL formulas can be reduced to the detection of these cycles. This "Emerson-Lei algorithm" is the standard cycle detection algorithm for transition graphs represented using binary decision diagrams, as in symbolic model checking. The paper also introduced the notion of alternation depth of fixpoint operators and showed that all common logics (e.g., CTL, CTL*) are in low alternation depth and have efficient model checkers. In recognition of the lasting contributions from this paper, Emerson and his student Lei won the very first instance of the now prestigious LICS Test-of-Time Award, in 2006.
  5. Emerson, E. Allen and A. Prasad Sistla, “Symmetry and Model Checking,” Formal Methods in System Design, 1996.This paper presented several techniques for utilizing symmetry among the processes of a concurrent system. These include quotient symmetry, an automata-based extension, and state symmetry. Symmetry allows reducing the verification complexity from exponential to polynomial in the number of processes, which is a major issue in dealing with the state explosion problem.
  6. Emerson, E. Allen and A. Prasad Sistla, “Utilizing Symmetry when Model-Checking under Fairness Assumptions: An Automata-Theoretic Approach,” ACM Transactions on Programming Languages and Systems, Vol. 19 (1997), Num. 4, pp. 617-638.This paper addresses combining model checking under symmetry with reasoning about liveness properties, which typically require fairness constraints. Protocols with 150 processes and 1047 states could be handled in less than an hour.
  7. Emerson, E. Allen and Kedar S. Namjoshi, “Verification of Parameterized Bus Arbitration Protocol,” Computer Aided Verification, 1998.This paper applies the paradigm of "any-size model checking" to an automotive communications protocol from Motorola.
  8. Emerson, E. Allen and Charanjit S. Jutla, “The Complexity of Tree Automata and Logics of Programs,” SIAM Journal of Computing, 1999.Tree automata are finite-state automata that operate on tree structures rather than linear input strings.  This paper establishes precise complexity bounds for the problem of checking emptiness of the language of tree automata, a central question in automata-theoretic model checking. This improved earlier results by an exponential order.
  9. Emerson, E. Allen, John Havlicek and Richard J. Trefler, “Virtual Symmetry Reduction,” Logic in Computer Science, 2000.This paper generalizes the concepts of symmetry reduction to virtual symmetry, so symmetry reduction can be applied to technically non-symmetric but nearly symmetric programs.
  10. Emerson, E. Allen and Thomas Wahl, “Dynamic Symmetry Reduction,” Tools and Algorithms for the Construction and Analysis of Systems, 2005.This paper builds on the theoretical ideas of symmetry reduction introduced in reference 5 above. It demonstrates how they can be applied to checking symbolic models that are based on binary decision diagrams (BDDs). This had been an open problem for about a decade, when it was shown that BDDs are provably unsuitable as a representation of a symmetry-reduced program model. This paper presents an alternative algorithm that does not require such a reduced model.
  11. Deshmukh, Jyotirmoy V., E. Allen Emerson and Prateek Gupta, “Automatic Verification of Parameterized Data Structures,” Tools and Algorithms for the Construction and Analysis of Systems, 2006.This paper presents a method of model checking that certain operations performed on linked data structures of any size preserve certain desirable properties. Operations might include the insertion of elements into a list or a tree; properties might be the acyclicity of the list, or the connectedness of the tree nodes. This paper unconventionally applies methods from parameterized verification and automata theory to the new field of software verification.
  12. Clarke, Edmund M., E. Allen Emerson and Joseph Sifakis,” Model checking: algorithmic verification and debugging,” Communications of the ACM, 2009.
  13. Hoffman, Leah, “Q&A: Talking Model Checking Technology, with Ed Clarke, E Allen Emerson, Joseph Sifakis, Winners of the 2007 Turing Award,” Communications of the ACM, 2008.This is the official Turing Award paper, and is a good intuitive introduction to historical and current topics in model checking.