ATTEND THE A.M. TURING CENTENARY
CELEBRATION!

MORE ACM AWARDS

HOME

Search

A.M. TURING AWARD WINNERS BY...

·       ALPHABETICAL LISTING

·       YEAR OF THE AWARD

·       RESEARCH SUBJECT

PHOTOGRAPHS

BIRTH:

2 June, 1954, Dallas/TX, USA

EDUCATION:

B.S. in Mathematics, University
of Texas at Austin, (1976); Ph.D. in Applied Mathematics, Harvard University
(1981).

EXPERIENCE:

Professor of Computer Science, University of Texas at Austin,
1981 onwards

HONORS AND AWARDS:

ACM Paris Kanellakis
Theory and Practice Award, (1998); CMU Allen Newell Award for Research
Excellence, (1999); IEEE Logic in Computer Science Test-of-Time Award (2006);
ACM A. M. Turing Award (2007).

E. Allen (Ernest Allen Emerson II)
Emerson

United States – 2007

CITATION

Together with Edmund Clarke and
Joseph Sifakis, for their role in developing Model[VAC1] -Checking into a highly effective verification technology
that is widely adopted in the hardware and software industries.

Press Release

·
Short Annotated

Bibliography

·
ACM DL

Author Profile

·
ACM Turing Award

Lecture Video

·
Research

Subjects

·
Additional

Materials

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[VAC2] . 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. A more technical
discussion of model checking can be found here.

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.

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

Emerson 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 1970's
at the University of Texas. He was also intrigued by the work of Jaco De Bakker, Willem-Paul De Roever,
and Edsger W Dijkstra on predicate transformers.

.

Emerson's
initial work[VAC3] .

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 essentially the same idea

This model checking method had several desirable
characteristics:

it was fully automatable and
algorithmic, since it entailed a systematic search of the program's state
space;

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;

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.

Later Work

Emerson’s essential and 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[VAC4] [VAC5] , as well as fixpoint logics are[VAC6]  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).

All model checkers must contend with efficiency issues. Early[VAC7]  model checkers typically computed every possible
configuration of values the program might assume. This could leads to a combinatorial
explosion in the size of the system state graph. Since the configuration of
program variables, including data values and location counters, is commonly
known as a state, this is referred to as the state explosion
problem. For example,
a concurrent system with 50 similar processes each having 10 local states might
have as many as 10**50 global states. As the field progressed, a number of
techniques were devised
to ameliorate state explosion, but state explosion has not been completely
vanquished. All model checkers must still contend with it to some extent for
extremely large and complicated programs[VAC8] .

Interestingly, there can also be a combinatorial
explosion in the size of the specification for some logics. In[VAC9]  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.

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.

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, and Spin from JPL. 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 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

·

LEARN MORE

ABOUT THE

A.M. TURING

AWARD

·       VIDEO:

THE ORIGINS

OF THE AWARD

·       2011 A.M. TURING

AWARD WINNER:

judea pearl

·       THE A.M. TURING AWARD

LECTURES

ACM (www.acm.org) is widely recognized as the
premier organization for computing professionals, delivering a broad array of
resources that advance the computing and IT disciplines, enable professional
development, and promote policies and research that benefit society.

© 2012 Association for Computing Machinery. All rights reserved.

[VAC1]Model
Checking

[VAC2]expressed as a temporal logic
formula

[VAC3]In a
seminal paper [2]
written in 1981, Emerson, in collaboration with  Clarke, co-founded the now
burgeoning field of model checking.  This paper originated   the technical  and conceptual  basis of an automated quality assurance
method that checks if  a nominally
finite state concurrent The original paper defined a verification method to
check whether a given candidate model—a finite state program—met a
given logical specification

[VAC4]such as CTL*

[VAC5]Model
checking was conceived from the beginning to provide the basis of a practical
verification method. Independently, in France during the same period, Sifakis originated a very similar idea, and thus co-founded
the growing field of model checking.

[VAC6]including certain fragments of the μ-calculus,

[VAC7]Although
the 1981 paper [2]
demonstrated that model checking was possible in principle, its application to
practical systems was severely limited. The most pressing limitation was the
need to search a huge number of states.

[VAC8]The [VAC8] most basic
entails abstraction which is replacement of the original, large program state
graph by a reduced state graph which captures some but not all of the original
information. For instance, under appropriate conditions, it can turn out that  the system
simplified to 5 processes and just 10**5 global states is behaviorally
equivalent and can be model checked instead.

[VAC9]and the size of the specification.