Skip to main content

E. Allen Emerson

Professor Emeritus

Emerson is noted for the invention and development of model checking, an algorithmic methods of verifying nominally finite state programs, originally proposed in a paper with Clarke in 1981. He has played a central role in its development through improved model checking algorithms, and new techniques for reductions in the site graph. He he has also made substantive contributions to program synthesis and automata theory.

Research

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, A. Prasad Sistla. 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.

Contact Info

E. Allen Emerson
Regents Chair Emeritus in Computer Science #2
Homepage
(512) 471-9537
emerson@cs.utexas.edu
GDC 5.432