E. Allen Emerson

E. Allen Emerson
Emerson in 2022
Born(1954-06-02)June 2, 1954
Dallas, Texas, U.S.
DiedOctober 15, 2024(2024-10-15) (aged 70)
Austin, Texas, U.S.
Education
Known for
Awards
Scientific career
FieldsComputer science
InstitutionsUniversity of Texas at Austin
Doctoral advisorEdmund M. Clarke

Ernest Allen Emerson II (June 2, 1954 – October 15, 2024) was an American computer scientist and winner of the 2007 Turing Award. He was Professor and Regents Chair at the University of Texas at Austin.

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]

  1. ^ "E. Allen Emerson - A.M. Turing Award Laureate". amturing.acm.org. Retrieved September 2, 2022.
  2. ^ Clarke, Edmund M.; Emerson, E. Allen (1982). "Design and synthesis of synchronization skeletons using branching time temporal logic". In Kozen, Dexter (ed.). Logics of Programs. Lecture Notes in Computer Science. Vol. 131. Berlin, Heidelberg: Springer. pp. 52–71. doi:10.1007/BFb0025774. ISBN 978-3-540-39047-3.
  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. ^ "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.