Ernest Allen Emerson II (born June 2, 1954), better known as E. Allen Emerson, is an American
computer scientist
A computer scientist is a person who is trained in the academic study of computer science.
Computer scientists typically work on the theoretical side of computation, as opposed to the hardware side on which computer engineers mainly focus (al ...
and winner of the 2007
Turing Award
The ACM A. M. Turing Award is an annual prize given by the Association for Computing Machinery (ACM) for contributions of lasting and major technical importance to computer science. It is generally recognized as the highest distinction in compu ...
. He is Professor and Regents Chair Emeritus at the
University of Texas at Austin
The University of Texas at Austin (UT Austin, UT, or Texas) is a public research university in Austin, Texas. It was founded in 1883 and is the oldest institution in the University of Texas System. With 40,916 undergraduate students, 11,075 ...
, United States.
Emerson is credited together with
Edmund M. Clarke
Edmund Melson Clarke, Jr. (July 27, 1945 – December 22, 2020) was an American computer scientist and academic noted for developing model checking, a method for formally verifying hardware and software designs. He was the FORE Systems Professor ...
and
Joseph Sifakis
Joseph Sifakis (Greek: Ιωσήφ Σηφάκης) is a Greek- French computer scientist. He received the 2007 Turing Award, along with Edmund M. Clarke and E. Allen Emerson, for his work on model checking.
Biography
Joseph Sifakis was born in He ...
for the invention and
development of
model checking
In computer science, model checking or property checking is a method for checking whether a finite-state model of a system meets a given specification (also known as correctness). This is typically associated with hardware or software systems ...
, a technique used in
formal verification
In the context of hardware and software systems, formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal metho ...
of software and hardware.
His contributions to
temporal logic In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am ''always'' hungry", "I will ''eventually'' be hungry", or "I will be hungry ''until'' I ...
and
modal logic
Modal logic is a collection of formal systems developed to represent statements about necessity and possibility. It plays a major role in philosophy of language, epistemology, metaphysics, and natural language semantics. Modal logics extend other ...
include the introduction of
computation tree logic (CTL) and its extension
CTL* CTL* is a superset of computational tree logic (CTL) and linear temporal logic (LTL). It freely combines path quantifiers and temporal operators. Like CTL, CTL* is a branching-time logic. The formal semantics of CTL* formulae are defined with resp ...
,
which are used in the verification of
concurrent systems
In computer science, concurrency is the ability of different parts or units of a program, algorithm, or problem to be executed out-of-order or in partial order, without affecting the outcome. This allows for parallel execution of the concurr ...
.
He is also credited along with others for developing
symbolic model checking to address
combinatorial explosion that arises in many model checking algorithms.
Early life and education
Emerson was born in
Dallas
Dallas () is the List of municipalities in Texas, third largest city in Texas and the largest city in the Dallas–Fort Worth metroplex, the List of metropolitan statistical areas, fourth-largest metropolitan area in the United States at 7.5 ...
,
Texas
Texas (, ; Spanish language, Spanish: ''Texas'', ''Tejas'') is a state in the South Central United States, South Central region of the United States. At 268,596 square miles (695,662 km2), and with more than 29.1 million residents in 2 ...
. His early experiences with computing included exposure to
BASIC
BASIC (Beginners' All-purpose Symbolic Instruction Code) is a family of general-purpose, high-level programming languages designed for ease of use. The original version was created by John G. Kemeny and Thomas E. Kurtz at Dartmouth College ...
,
Fortran, and
ALGOL 60
ALGOL 60 (short for ''Algorithmic Language 1960'') is a member of the ALGOL family of computer programming languages. It followed on from ALGOL 58 which had introduced code blocks and the begin and end pairs for delimiting them, representing a k ...
on the
Dartmouth Time Sharing System and
Burroughs large systems
The Burroughs Large Systems Group produced a family of large 48-bit mainframes using stack machine instruction sets with dense syllables.E.g., 12-bit syllables for B5000, 8-bit syllables for B6500 The first machine in the family was the B5000 in ...
computers.
[
He went on to receive a ]Bachelor of Science
A Bachelor of Science (BS, BSc, SB, or ScB; from the Latin ') is a bachelor's degree awarded for programs that generally last three to five years.
The first university to admit a student to the degree of Bachelor of Science was the University of ...
degree in mathematics from the University of Texas at Austin
The University of Texas at Austin (UT Austin, UT, or Texas) is a public research university in Austin, Texas. It was founded in 1883 and is the oldest institution in the University of Texas System. With 40,916 undergraduate students, 11,075 ...
in 1976 and a Doctor of Philosophy
A Doctor of Philosophy (PhD, Ph.D., or DPhil; Latin: or ') is the most common Academic degree, degree at the highest academic level awarded following a course of study. PhDs are awarded for programs across the whole breadth of academic fields ...
degree in applied mathematics at Harvard University
Harvard University is a private Ivy League research university in Cambridge, Massachusetts. Founded in 1636 as Harvard College and named for its first benefactor, the Puritan clergyman John Harvard, it is the oldest institution of higher le ...
in 1981.[
]
Career
In the early 1980s, Emerson and his PhD advisor, Edmund M. Clarke, developed techniques for verifying a finite-state system against a formal specification. They coined the term ''model checking'' for the concept, which was independently studied by Joseph Sifakis in Europe.[ This sense of the word ''model'' matches the usage from ]model theory
In mathematical logic, model theory is the study of the relationship between formal theories (a collection of sentences in a formal language expressing statements about a mathematical structure), and their models (those structures in which the s ...
in mathematical logic
Mathematical logic is the study of logic, formal logic within mathematics. Major subareas include model theory, proof theory, set theory, and recursion theory. Research in mathematical logic commonly addresses the mathematical properties of for ...
: the system is called a ''model'' of the specification.
Emerson's work on model checking included early and influential temporal logic In logic, temporal logic is any system of rules and symbolism for representing, and reasoning about, propositions qualified in terms of time (for example, "I am ''always'' hungry", "I will ''eventually'' be hungry", or "I will be hungry ''until'' I ...
s for describing specifications, and techniques for reducing state space explosion.[
]
Awards
In 2007, Emerson, Clarke, and Sifakis won the Turing award.[ The citation reads:
In addition to the Turing award, Emerson received the 1998 ]ACM
ACM or A.C.M. may refer to:
Aviation
* AGM-129 ACM, 1990–2012 USAF cruise missile
* Air chief marshal
* Air combat manoeuvring or dogfighting
* Air cycle machine
* Arica Airport (Colombia) (IATA: ACM), in Arica, Amazonas, Colombia
Computing
* ...
Paris Kanellakis Award,
together with Randal Bryant
Randal E. Bryant (born October 27, 1952) is an American computer scientist and academic noted for his research on formally verifying digital hardware and software. Bryant has been a faculty member at Carnegie Mellon University since 1984. He ser ...
, Clarke, and Kenneth L. McMillan for the development of symbolic model checking.[ The citation reads:
]
See also
* List of pioneers in computer science
References
External links
E. Allen Emerson homepage
at the University of Texas at Austin
*
{{DEFAULTSORT:Emerson, E. Allen
Living people
University of Texas at Austin College of Natural Sciences alumni
Harvard University alumni
University of Texas at Austin faculty
American computer scientists
Turing Award laureates
Formal methods people
1954 births