E. Allen Emerson
Ernest Allen Emerson II was an American computer scientist and winner of the 2007 Turing Award. He was a professor at the University of Texas at Austin from 1981 to 2016.
Emerson is credited together with Edmund M. Clarke and Joseph Sifakis for the invention and development of model checking, a technique used in formal verification of software and hardware. His contributions to temporal logic and modal logic include the introduction of computation tree logic and its extension CTL*, which are used in the verification of concurrent systems. He is also recognized 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, Texas, on June 2, 1954. His early experiences with computing included exposure to BASIC, Fortran, and ALGOL 60 on the Dartmouth Time-Sharing System and Burroughs large systems computers.He went on to receive a Bachelor of Science degree in mathematics from the University of Texas at Austin in 1976 and a Doctor of Philosophy degree in applied mathematics at Harvard University 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.Emerson's work on model checking included early and influential temporal logics for describing specifications, and techniques for reducing state space explosion.
Emerson joined the department of computer science at the University of Texas at Austin shortly after his graduation in 1981. He taught at the university for 35 years.
Emerson retired in 2016 from UT Austin. He held the title of Regents Chair Emeritus.
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,
together with Randal Bryant, Clarke, and Kenneth L. McMillan for the development of symbolic model checking. The citation reads: