E. Allen Emerson

In 1981, Edmund M. Clarke and E. Allen Emerson working in the USA, and Joseph Sifakis working independently in France, authored seminal papers that founded what has become the highly successful field of Model Checking. This verification technology provides an algorithmic means of determining whether an abstract model representing, for example, a hardware or software design, satisfies a formal specification expressed in temporal logic. Moreover, if the property does not hold, the method identifies a counterexample that shows the source of the problem. The progression of Model Checking to the point where it can be successfully used for complex systems has required the development of sophisticated means of coping with what is known as the “state explosion problem”. Great strides have been made on this problem since 1981 by what is now a very large international research community. As a result, many major hardware and software companies are now using Model Checking in practice. Examples of its use include the verification of VLSI circuits, communication protocols, software device drivers, real-time embedded systems, and security algorithms.

The work of Drs. Clarke, Emerson, and Sifakis has been central to the success of this research area. Their work over the years has led to the creation of new logics for specification, new verification algorithms, and surprising theoretical results. Model Checking tools, created by both academic and industrial teams, have resulted in an entirely novel approach to verification and test case generation. This approach, for example, often enables engineers in the electronics industry to design complex systems and have considerable assurance regarding the correctness of their designs.

Life

E. Allen Emerson II was born and grew up in Dallas, Texas. He was always interested in scientific and mathematical topics. He taught himself calculus several years before he took it in public school. Emerson took a course on computer programming in high school, and learned BASIC on a GE Mark I Time Sharing System. Subsequently, he taught himself Fortran and Algol (from the Algol 60 report), and ran programs on a Burroughs B5500 mainframe computer.

Emerson studied as an undergraduate at the University of Texas in Austin, where he earned his B.S. in Mathematics in 1976. He went on to graduate school at Harvard University, obtaining a Ph.D. in Applied Mathematics (Computer Science) in 1981. Shortly thereafter he joined the University of Texas in Austin as a faculty member, and has remained there since. He is now Regents Chair and Professor of Computer Science.

He has an interest in formal methods for establishing program correctness that dates back to his college days. This was inspired in part by reading a Communications of the ACM 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 the 1970's at the University of Texas. He was also intrigued by the work of J. W. De Bakker, W. P De Roever, and Edsger W. Dijkstra on predicate transformers.

Emerson is an Highly Cited Researcher of the Information Sciences Institute, a recognition given to the 250 most referenced computer science researchers. He has served as editor for leading formal methods journals, including ACM Transactions on Computational Logic (ToCL), Formal Methods in Systems Design (FMSD), Formal Aspects of Computing (FAC), and Methods of Logic in Computer Science (MLCS). He is a founding member of the steering committee for the formal methods conference Automated Tools for Verification and Analysis (ATVA), and he serves on the steering committee of Verification, Model Checking, and Abstract Interpretation (VMCAI).

A description of Emerson's technical work can be found here.

Author: Thomas Wahl