Brief Biography

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 proposed an algorithmic method of verifying nominally finite-state concurrent programs, called model checking, in a paper with Ed Clarke in 1981. 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 Prize, and the IEEE LICS'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, and ranks in the top 1% of the most cited computer scientists on CiteSeer.

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. 

Publications 

• Research Papers  
• Books, Chapters, Expository, and Invited Works 
• Other papers

Of   Note 

• 25MC pre-print  
• Some early notes on model checking 
• An early draft of [CE81]
• [CE81]

Courses

• CS378 (a undergraduate course in Debugging and Verification of Programs) 
• CS388S (a graduate breadth course in Formal Verification and Semantics) 
• CS388F (a graduate breadth course in Automata and Formal Language Theory) 
• CS395T (a graduate seminar in Model Checking and Automated Formal Methods) 
• CS353 (an undergraduate course in the Theory of Computing)

Students

• Jyotirmoy Deshmukh
• Subramanian Iyer 
• Roopsha Samanta
• Thomas Wahl