Remembering Turing Award Winner E. Allen Emerson
Emerson was a pioneer of a computer science technique called Model Checking that has become a standard approach in hardware and software development.
E. Allen Emerson
E. Allen Emerson, winner of the most prestigious award in computer science and a faculty member at The University of Texas at Austin since 1981, died on October 16 after an extended illness.
Along with Edmund M. Clarke and Joseph Sifakis, Emerson was awarded the 2007 A.M. Turing Award by the Association for Computing Machinery, the highest honor in computer science, for research in an automatic verification technique known as Model Checking. Their innovations transformed this approach from a theoretical technique to a highly effective verification technology that enables computer hardware and software engineers to find errors efficiently in complex system designs. This transformation resulted in increased assurance that the systems perform as intended by the designers, using a fully automated approach that is now the most widely used verification method in the hardware and software industries.
“Allen’s work was a huge step forward in the development of tools that help designers create systems with known, verifiable properties,” said Don Fussell, chair of the Department of Computer Science. “Without tools like these, we’re simply out of our depth designing systems of the complexity of today’s computing systems or, indeed, other types of systems of similar complexity. On top of this impact, the quality of his work represents the high standard of excellence our faculty expect from ourselves at our best. He will be sorely missed.”
Model Checking as a standard procedure for quality assurance has enabled designers and manufacturers to address verification problems that span both hardware and software. It has also helped them to gain mathematical confidence that complex computer systems meet their specifications, and it has provided added security for a range of both common and critical computing applications. Many major hardware and software companies now rely heavily on Model Checking. Common examples include verification of the designs for integrated circuits such as microprocessors, as well as communication protocols, software device drivers, real-time embedded systems and security algorithms.
Born and raised in Dallas, Texas, Emerson had an early interest in scientific and mathematical topics. He taught himself calculus several years before he took it in public school. He took a course on computer programming in high school, where he learned the BASIC programming language. Subsequently, he taught himself Fortran and Algol, running programs on a mainframe computer.
Emerson received a bachelor’s degree in mathematics from The University of Texas at Austin, and a doctoral degree in applied mathematics from Harvard University before joining the Computer Science department at UT as an assistant professor in 1981. He spent his academic career at UTCS, retiring in 2016 as Regents Chair Emeritus.
In addition to the Turing Award, Emerson was co-recipient of the 1998 Paris Kanellakis Award for Theory and Practice from the ACM, the Allen Newell Award for Research Excellence from Carnegie Mellon University and the 2006 Test-of-Time Award from the IEEE Symposium on Logic in Computer Science (LICS) for his research on efficient Model Checking.
