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 (a ...
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 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 ...
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 system ...
, 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 met ...
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 ot ...
include the introduction of
computation tree logic
Computation tree logic (CTL) is a branching-time logic, meaning that its model of time is a tree-like structure in which the future is not determined; there are different paths in the future, any one of which might be an actual path that is realiz ...
(CTL) and its extension
CTL*,
which are used in the verification of
concurrent systems.
He is also credited along with others for developing
symbolic model checking to address
combinatorial explosion
In mathematics, a combinatorial explosion is the rapid growth of the complexity of a problem due to how the combinatorics of the problem is affected by the input, constraints, and bounds of the problem. Combinatorial explosion is sometimes used to ...
that arises in many model checking algorithms.
Early life and education
Emerson was born in
Dallas
Dallas () is the third largest city in Texas and the largest city in the Dallas–Fort Worth metroplex, the fourth-largest metropolitan area in the United States at 7.5 million people. It is the largest city in and seat of Dallas County ...
,
Texas
Texas (, ; Spanish: ''Texas'', ''Tejas'') is a state in the South Central region of the United States. At 268,596 square miles (695,662 km2), and with more than 29.1 million residents in 2020, it is the second-largest U.S. state by ...
. 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 ...
on the
Dartmouth Time Sharing System
The Dartmouth Time-Sharing System (DTSS) is a discontinued operating system first developed at Dartmouth College between 1963 and 1964. It was the first successful large-scale time-sharing system to be implemented, and was also the system for wh ...
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 ...
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 o ...
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 degree at the highest academic level awarded following a course of study. PhDs are awarded for programs across the whole breadth of academic fields. Because it is ...
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 highe ...
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
In computer science, formal specifications are mathematically based techniques whose purpose are to help with the implementation of systems and software. They are used to describe a system, to analyze its behavior, and to aid in its design by verif ...
. 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 theory (mathematical logic), formal theories (a collection of Sentence (mathematical logic), sentences in a formal language expressing statements about a Structure (math ...
in mathematical logic
Mathematical logic is the study of 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 forma ...
: 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 ]Paris Kanellakis Award The Paris Kanellakis Theory and Practice Award is granted yearly by the Association for Computing Machinery (ACM) to honor "specific theoretical accomplishments that have had a significant and demonstrable effect on the practice of computing". It wa ...
,
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
This is a list of people who made transformative breakthroughs in the creation, development and imagining of what computers could do.
Pioneers
: ''To arrange the list by date or person (ascending or descending), click that column's small "up-do ...
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