E. Allen Emerson

Professor Emeritus
Emerson is co-inventor and co-developer of model checking, an algorithmic method of verifying nominally finite-state concurrent programs authored with Ed Clarke in 1981. His other contributions include new and improved model checking algorithms, abstractions and reductions to simplify the complexity of model checking, decision procedures, and algorithmic methods of program synthesis. Emerson is a recipient of the ACM Turing Award, as well as the ACM Kanellakis Prize, the CMU Newell Medal, and the IEEE LI.CS'06 Test-of-Time Award.


Research Areas:
Research Interests: 
  • Establishing program correctness
    • including logics and semantics of programs and concurrent and distributed computing

Select Publications

Edmund M. Clarke, E. Allen Emerson, Joseph Sifaki. 2009. Model checking: algorithmic verification and debugging.
Jyotirmoy V. Deshmukh, E. Allen Emerson, Prateek Gupta. 2006. Automatic Verification of Parameterized Data Structures.
E. Allen Emerson, Charanjit S. Jutla. 1998. The Complexity of Tree Automata and Logics of Programs.
E. Allen Emerson, Charanjit S. Jutla. 1996. Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-Theoretic Approach.
E. Allen Emerson, Chin-Laung Lei. 1986. Efficient Model Checking in Fragments of the Propositional Mu-Calculus.