Ernest Allen Emerson II was born on June 2, 1954, and passed away on October 15, 2024. He was an American computer scientist who received the 2007 Turing Award. He taught at the University of Texas at Austin from 1981 to 2016.

Emerson worked with Edmund M. Clarke and Joseph Sifakis to create and improve model checking, a method used to check if software and hardware function correctly. His work in temporal logic and modal logic included developing computation tree logic (CTL) and its expanded version, CTL*, which are used to test systems that run multiple tasks at the same time. He and others are also known for creating symbolic model checking, a technique designed to solve problems caused by the large number of possibilities in model checking processes.

Early life and education

Emerson was born in Dallas, Texas, on June 2, 1954. He learned about computer programming languages like BASIC, Fortran, and ALGOL 60 using the Dartmouth Time-Sharing System and large computers made by Burroughs. He earned a Bachelor's degree in mathematics from the University of Texas at Austin in 1976 and a Doctorate degree in applied mathematics from Harvard University in 1981.

Career

In the early 1980s, Emerson and his PhD advisor, Edmund M. Clarke, created methods to check if a system with a limited number of states met clearly defined rules. They introduced the term "model checking" for this process, which was also studied separately by Joseph Sifakis in Europe.

Emerson’s research on model checking included early and important logics that describe how things change over time, as well as methods to address the challenge of managing too many possible states to analyze.

After graduating in 1981, Emerson began working in the computer science department at the University of Texas at Austin. He taught there for 35 years.

Emerson retired from the University of Texas at Austin in 2016. At that time, he held the title of Regents Chair Emeritus.

Awards

In 2007, Emerson, Clarke, and Sifakis received the Turing Award. The description states:

In 1998, Emerson also received the ACM Paris Kanellakis Award, along with Randal Bryant, Clarke, and Kenneth L. McMillan. This award was given for creating symbolic model checking. The description states: