The 2007 Turing Award recognized the work of E. Allen Emerson for transforming model checking from a theoretical concept into a vital verification technology. His contributions provided the industry with robust methods to ensure the reliability of complex software and hardware systems, cementing his role as a primary figure in the development of formal verification.
Academic Background
Born in Dallas on June 2, 1954, Emerson gained early exposure to programming through BASIC, Fortran, and ALGOL 60. He pursued higher education at the University of Texas at Austin, earning a Bachelor of Science in mathematics in 1976. He later attended the Harvard School of Engineering and Applied Sciences, where he completed his Doctor of Philosophy in applied mathematics in 1981.
Twenty questions, eight minutes on the clock, and a percentile measured against everyone who has taken it. No sign-up.
Take the IQ test →Development of Model Checking
During his time at Harvard, Emerson worked with his PhD advisor, Edmund M. Clarke, to create techniques for verifying finite-state systems against formal specifications. This collaboration led to the inception of model checking. Emerson specifically introduced computation tree logic and its extension, CTL*, to describe specifications for concurrent systems. He also collaborated on the development of symbolic model checking, a method designed to mitigate the combinatorial explosion problems inherent in traditional verification algorithms.
Professional Tenure and Recognition
Emerson joined the computer science faculty at the University of Texas at Austin in 1981. He maintained this position for 35 years, educating students until his retirement in 2016, when he was named Regents Chair Emeritus. His research efforts received significant recognition, including the 1998 ACM Paris Kanellakis Award, which he shared with Randal Bryant, Clarke, and Kenneth L. McMillan for their advancements in symbolic model checking.
Fast facts
- Born: June 2, 1954, Dallas, United States
- Died: October 15, 2024, Austin, United States
- Education: University of Texas at Austin, Harvard University
- Turing Award: 2007
- Paris Kanellakis Award: 1998
- Academic Title: Regents Chair Emeritus
Questions readers ask
What is model checking?
It is a formal verification technique used to verify hardware and software system designs against specifications.
Which major academic awards did Emerson receive?
He received the Paris Kanellakis Award in 1998 and the Turing Award in 2007.
Achievements
- Turing Award — 2007
- Affiliated with University of Texas at Austin
- Educated at University of Texas at Austin and Harvard School of Engineering and Applied Sciences
- Worked as computer scientist, engineer and university teacher
