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 is the inventor of model checking ,
an algorithmic method of verifying nominally finite-state concurrent programs,
in a paper he wrote, but published jointly. [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.
He received his B.S. degree from the University of Texas at Austin in
Mathematics and a Ph.D. in Applied Mathematics from Harvard
New   and   Notable