E. Allen Emerson, professor of computer sciences at The University of Texas at Austin, has been awarded the 2007 A.M. Turing Award, widely considered the most prestigious award in computing, for original and continuing research in a quality assurance process known as “Model Checking.”
Emerson received the award, given annually by the Association for Computing Machinery (ACM), with collaborator Edmund Clarke, of Carnegie Mellon University, and Joseph Sifakis who worked independently for the Centre National de la Recherche Scientifique at the University of Grenoble in France.
Their innovations transformed the Model Checking 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 has resulted in increased assurance that the systems perform as intended by the designers.
ACM President Stuart Feldman said the work of Clarke, Emerson and Sifakis has had a major impact on designers and manufacturers of semiconductor chips.
“These industries face a technology explosion in which products of unprecedented complexity have to operate as expected for companies to survive,” said Feldman. “This verification advance enabled these industries to shorten time to market and increase product integrity.”
Many major hardware and software companies now rely heavily on Model Checking. Among the beneficiaries of Model Checking are personal computer users, medical device makers and nuclear power plant operators. Wherever significant investments or human lives are at risk, quality assurance for the pervasive underlying hardware and software becomes paramount.
The Turing Award carries a $250,000 prize with financial support provided by Intel Corporation and Google Inc.
ACM will present the award at its annual awards banquet on June 21 in San Francisco.
Emerson is an endowed professor in the Department of Computer Sciences. He was a co-recipient of the 2006 Test-of-Time Award from the IEEE Symposium on Logic in Computer Science (LICS) for his research on efficient Model Checking in the propositional mu-calculus, a highly expressive temporal logic, with Chin-Laung Lei.
He has served on the editorial boards of several leading journals in applied logic and formal methods and is on the steering committee of the International Symposium on Automated Technology for Verification and Analysis and the International Conference on Verification, Model Checking, and Abstract Interpretation.
Emerson received a bachelor’s degree in mathematics from The University of Texas at Austin, and a doctor’s degree in applied mathematics from Harvard University.
