E. Allen Emerson
Born (1954-06-02) June 2, 1954
Dallas, Texas
CitizenshipUnited States
Education
Known for
Awards
Scientific career
FieldsComputer science
InstitutionsUT Austin, United States
Doctoral advisorEdmund M. Clarke

Ernest Allen Emerson II (born June 2, 1954), better known as E. Allen Emerson, is an American computer scientist and winner of the 2007 Turing Award. He is Professor and Regents Chair Emeritus at the University of Texas at Austin, United States.

Emerson is recognized 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.[1] His contributions to temporal logic and modal logic include the introduction of computation tree logic (CTL)[2] and its extension CTL*,[3] 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.[4]

Early life and education

Emerson was born in Dallas, Texas. His early experiences with computing included exposure to BASIC, Fortran, and ALGOL 60 on the Dartmouth Time Sharing System and Burroughs large systems computers.[1] 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.[1]

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.[1] This sense of the word model matches the usage from model theory in mathematical logic: the system is called a model of the specification.

Emerson's work on model checking included early and influential temporal logics for describing specifications, and techniques for reducing state space explosion.[1]

Awards

In 2007, Emerson, Clarke, and Sifakis won the Turing award.[1] The citation reads:

for their role in developing Model-Checking into a highly effective verification technology that is widely adopted in the hardware and software industries.

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.[4] The citation reads:

For their invention of symbolic model checking, a method of formally checking system designs, which is widely used in the computer hardware industry and is beginning to show significant promise also in software verification and other areas.

See also

References

  1. 1 2 3 4 5 6 "E. Allen Emerson - A.M. Turing Award Laureate". amturing.acm.org. Retrieved September 2, 2022.
  2. ↑ Clarke, Edmund M.; Emerson, E. Allen (1982). Kozen, Dexter (ed.). Design and synthesis of synchronization skeletons using branching time temporal logic. Lecture Notes in Computer Science. Vol. 131. Berlin, Heidelberg: Springer. pp. 52–71. doi:10.1007/BFb0025774. ISBN 978-3-540-39047-3. {{cite book}}: |journal= ignored (help)
  3. ↑ Emerson, E. Allen; Halpern, Joseph Y. (January 2, 1986). ""Sometimes" and "not never" revisited: on branching versus linear time temporal logic". Journal of the ACM. 33 (1): 151–178. doi:10.1145/4904.4999. ISSN 0004-5411. S2CID 10852931.
  4. 1 2 "AWARDS -- E. ALLEN EMERSON -- 'ACM A.M. Turing Award' and 'Paris Kanellakis Theory and Practice Award'". Association for Computing Machinery. 2015. Archived from the original on June 6, 2015. Retrieved July 21, 2015. […] authored seminal papers that founded what has become the highly successful field of Model Checking.
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.