E. Allen Emerson

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.

The Model Checking Approach

Working in North America in the early 1980's, Emerson, in collaboration with Edmund Clarke, originated the technical concepts of an automated quality assurance method that checks if a nominally finite state concurrent system provides a model of (i.e., satisfies) its specification. They also coined the now ubiquitous term Model Checking for the method. Working in Europe, Joseph Sifakis independently discovered a similar idea. This model checking method had several desirable characteristics:

1. it was fully automatable and algorithmic, since it entailed a systematic search of the program's state space;
2. it was precise and expressive, with a formally defined specification logic, Computation Tree Logic (CTL), that could capture a wide variety of correctness properties of interest;
3. it was efficient, having running time that is polynomial in the sizes of both the input system and the specification, partly owing to this particular logic;
4. it was very appropriate for reasoning about concurrent programs, for which traditional quality assurance methods had proven largely ineffective;
5. it was conceived from the beginning to provide a practical basis for a practical verification method.

Emerson’s path-breaking contributions to the development of model checking include the formulation of widely used logics for flexible and expressive specifications as well as associated model checking algorithms. The expressiveness of powerful computation tree logics, as well as fixpoint logics are fundamental in both theory and practice. Arguably, expressiveness is even more basic than the efficiency for reasoning methods: if the important correctness properties cannot even be expressed, the logics are not useful for program verification. Much of the logical machinery developed by Emerson is central to most industrial specification logics and related model checking tools. As a result, the logics have been incorporated into several prominent commercial frameworks (e.g. IBM Sugar) and engineering standards for specification (e.g. Accellera-IEEE Property Specification Logic, IBM Property Specification Logic/Sugar).

The original paper [2] described the basic principles of model checking. However, it and all subsequent model checkers must contend with efficiency issues. Intuitively, the problem is that small programs can have an extremely large number of states, i.e. configurations of program variables including data values and location counters. Early model checkers typically computed every possible state of the program. This could lead to a combinatorial blowup in the size of the system state graph known by the term state explosion. For example, a concurrent system with 50 similar processes each having just 10 local states might have an astronomical 10**50 global states. As the field progressed, a number of powerful techniques were devised to ameliorate state explosion, often based on simplifying or shrinking the representation of the state graph. Consequently, the size of systems amenable to model checking has increased enormously over the years. While state explosion has not been completely vanquished, it has been largely tamed for many applications.

Avoiding Combinatorial Explosion

As the long version of the A.M. Turing Award citation noted, "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."

In most cases the system size dominates, and even the exponential blow-up for a small specification in linear temporal logic might be tolerable. But in other cases the specification is large, resulting in a substantial (exponential or worse) blow-up that is not workable. Emerson's work addresses efficiency in both the system size and the specification size. An advantage of using logics such as CTL is that the cost of model checking is linear in the size of the specification.

Emerson has also made highly innovative and influential advances in techniques for limiting state explosion. One technique exploits the redundancy that results from the symmetry inherent in systems comprised of many copies of similar sub-components. This allows large systems to be converted into much smaller systems, permitting dramatic increases in the speed and capacity of model checkers. Symmetry reduction permits reasoning about a large model using an exponentially reduced model. Many model checking tools incorporate symmetry reduction, including Rulebase from IBM. Emerson has also been a pioneer in combining reductions with other means of combating state explosion, such as symmetry reduction with symbolic model representations, or symmetry reduction with partial order reduction.

Another line of Emerson's work has been an examination of a key component of some model checking approaches. This involved applying fixpoint logics to check non-emptiness of automata on infinite objects and calculate winning strategies for games between an open system and its environment. These have applications to model checking multi-agent systems. Work at the Weizmann Institute similarly employed computation tree logics for automatic program design, and more recently for compositional reasoning.

Another approach solves many important cases of the parameterized model checking problem, where one must establish correctness for systems comprised of n sub-components, for all n. Emerson has used these techniques to algorithmically verify an unboundedly long automotive data protocol for Motorola, and to verify arbitrarily large systems of common cache protocols.

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).

Author: Thomas Wahl