E. Allen Emerson

Regents Chair and Professor

Department of Computer Science
Gates-Dell Complex 3.720
The University of Texas at Austin
Austin, TX 78712 USA


512-471-9537 (office)
512-471-7316 (secretary)
512-471-8885 (fax)
Email: emerson at cs.utexas.edu  

Title: The Genesis and Development of Model Checking: Fact vs. Fiction

Speaker: Allen Emerson

Day: Wednesday, September 30

Clarke and Emerson are noted for the invention and development of model checking [CE81]. In this presentation, I will recall the roles of the principals. I was responsible for the initial conception of model checking, as a spinoff of my work on program synthesis. This entailed the checking of candidate models of a temporal specification algorithmically, and explains the coining of the term model checking. Model checking plainly was a form of verification circumventing proofs. As a part of some consulting work, Ed Clarke had been consulting on verification of protocols using temporal specifications and deductive proofs. As I discussed model checking with Ed, he envisioned that it could be a really practical verification method, applicable to protocols and more. Later, Ed commented that neither one of us could have achieved model checking without the other. <\p>

There are alternative perspectives on this history. In broad brush, these agree, but they vary in detail. I will elaborate with additional crucial facts, and examine their impact on various apparent discrepancies. I would like to suggest the relevance of Pnueli's Principle here: The junior researcher lives in the problem, while the senior researcher lives in a constant stream of interrupts. A Corollary is: The junior researcher will singlemindedly acquire a detailed memory concerning the problem and its solution; The overburdened, timesharing senior researcher will lack sufficient focused attention, blocks of time, and depth of understanding to have good recall.

[CE81] Edmund M. Clarke and E. Allen Emerson: Design and Synthesis of Synchronization Skeletons Using Branching-Time Temporal Logic. Logics of Programs, Workshop, Yorktown Heights, New York, May 1981

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 is co-inventor and co-developer of model checking , an algorithmic method of verifying nominally finite-state concurrent programs. The method was proposed in this paper [CE81]. authored with Ed Clarke in 1981, a paper widely recognized as seminal for founding today's broad field of model checking and establishing its basic principles. These 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 University.


New   and   Notable  



  • CS340D (a undergraduate course in Debugging and Verification of Programs) 
  • CS388S (a graduate breadth course in Formal Verification and Semantics) link
  • 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)


Current and Recent Ph.D. Students Prior Ph.D. Students
eXTReMe Tracker