Button to scroll to the top of the page.

E A Emerson

Professor Emeritus
Department of Computer Science

Regents Chair in Computer Sciences #2

Formal Methods


Postal Address
AUSTIN, TX 78701

Research Interests

Dr. E. Allen Emerson has a longstanding interest in formal methods for establishing program correctness. This was inspired in part by reading in the mid-1970's a CACM paper by Tony Hoare "Proof of Program: Find". Also inspirational was a talk by Zohar Manna on fixpoints and the Tarski-Knaster Theorem given in 1975 at the University of Texas.

Emerson has been recognized as co-inventor of model checking , an algorithmic method of verifying nominally finite-state concurrent programs, proposed in this paper [CE81]. Such ongoing finite state programs correspond to the synchronization skeletons of many concurrent, distributed, or reactive programs comprised of multiple processes that must synchronize or coordinate their behavior. Correct behavior is described using a temporal logic, such as CTL (Computation Tree Logic) permitting specification of behavior along all futures versus some futures. In the past quarter century model checking has become a very popular and successful approach to formal verification. 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. Additional interests include model checking symmetric and nearly symmetric systems, verification of parameterized systems, and reasoning about data structures. 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. He serves on the editorial boards of leading formal methods journals as well as conference program committees. He is an Information Sciences Institute Highly Cited Researcher. Emerson is a member of the ACM.
He received his B.S. degree from the University of Texas at Austin in Mathematics and a Ph.D. in Applied Mathematics from Harvard University.

Selected Publications

Edmund M. Clarke, E. Allen Emerson, Joseph Sifakis. Model checking: algorithmic verification and debugging. Commun. ACM 52(11): 74-84 (2009)

Jyotirmoy V. Deshmukh, E. Allen Emerson, Prateek Gupta. Automatic Verification of Parameterized Data Structures. TACAS 2006: 27-41.

E. Allen Emerson, Charanjit S. Jutla. The Complexity of Tree Automata and Logics of Programs. SIAM J. Comput. 29(1): 132-158 (1999) 1998.

E. Allen Emerson, A. Prasad Sistla. Utilizing Symmetry when Model Checking under Fairness Assumptions: An Automata-Theoretic Approach. ACM Trans. Program. Lang. Syst. 19(4): 617-638 (1997) 1996.

E. Allen Emerson, Chin-Laung Lei. Efficient Model Checking in Fragments of the Propositional Mu-Calculus.LICS 1986: 267-278.

E. Allen Emerson, Edmund M. Clarke.Characterizing Correctness Properties of Parallel Programs Using Fixpoints.ICALP 1980: 169-181

E. Allen Emerson, Kedar S. Namjoshi (eds.). Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006. Charleston, SC, USA, January 8-10, 2006, Proceedings Springer 2006

E. Allen Emerson. Meanings of Model Checking. Concurrency, Compositionality, and Correctness. 237-249 (2010).

E. Allen Emerson. The Beginning of Model Checking: A Personal Perspective. 25 Years of Model Checking, 2006 (2008): 27-45.

E. Allen Emerson. Temporal and Modal Logic. Handbook of Theoretical Computer Science, Volume B: Formal Models and Semantics. 1990: 995-1072.

  • ACM A.M. Turing Award
  • ACM Paris Kanellakis Theory and Practice Award
  • CMU Allen Newell Award for Research Excellence
  • IEEE Logic in Computer Science Test-of-Time Award