ACM Turing Award Honors Founders of Automatic Verification Technology
ACM Turing Award Honors Founders of Automatic Verification Technology
Researchers Created Model Checking Technique for Hardware and Software Designers
The Association for Computing Machinery
Advancing Computing as a Science & Profession
Contact: Virginia Gold
212-626-0505
[email protected]
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. This verification advance enabled these industries to shorten time to market and increase product integrity. Without the conceptual breakthrough pioneered by these researchers, we might still be stuck with chips that have many errors and would lack the power and speed of today’s equipment. This is a great example of an industry-transforming technology arising from highly theoretical research," Feldman said.
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.
"Intel and the entire computing industry have been direct beneficiaries of the awardees' ground-breaking work,” said Andrew Chien, Vice President in the Corporate Technology Group and Director of Research of Intel Corporation. "Our researchers and engineers have worked closely with Clarke, Emerson, and Sifakis for 15 years. Insights from their novel automatic verification results have been widely adopted by the entire industry. These Model Checking approaches provide dramatically better coverage when searching for design errors."
"Google, like any contemporary technology company, owes a great deal of its success to the work of pioneering researchers who have come before," said Alan Eustace, Senior Vice President of Engineering at Google. "We are proud to honor the award winners for their innovative solution to a difficult and pervasive issue and we hope this will encourage and inspire those who now face the technology challenges of the future."
Migrating from Pure Research to Industrial Reality
Logical errors in digital circuit designs, software, and communication protocols are an important problem for system designers. They often result in delays in getting new products to market, failures of critical systems already in use, and expensive replacement of faulty hardware and patching of flawed software.
Model Checking started as an academic research idea. The continuing research of Clarke, Emerson, and Sifakis as well as others in the international research community over the last 27 years led to the creation of new logics, as well as new algorithms and surprising theoretical results. This in turn has stimulated the creation of many Model Checking tools by both academic and industrial teams, resulting in the widespread industrial use of Model Checking.
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.
Among the beneficiaries of Model Checking are personal computer users, medical device makers, and nuclear power plant operators. As computerized systems pervade daily life, consumers rely on digital controllers to supervise critical functions of cars, airplanes, and industrial plants. Digital switching technology has replaced analog components in the telecommunications industry, and security protocols enable e-commerce applications and privacy. Wherever significant investments or human lives are at risk, quality assurance for the underlying hardware and software components becomes paramount.
Background
In 1981, Edmund Clarke and Allen Emerson working in the U.S., and Joseph Sifakis working independently in France with J.P. Queille, authored seminal papers that founded what has become the highly successful field of Model Checking. This verification technology offers two advantages. It provides an algorithmic means of determining whether an abstract model, such as a hardware or software design, satisfies a formal specification, such as a temporal logic formula (i.e., a pattern for a sequence of events). In addition, it identifies the counter-examples that show the source of the problem, which must be addressed should the stated property specification not hold.
A drawback of the Model Checking approach, known as the state-explosion problem, seemed to limit its applicability to small designs of mainly academic interest. Randal Bryant, Edmund Clarke, Allen Emerson and Kenneth McMillan invented Symbolic Model Checking, which greatly extended the size and complexity of systems that could be verified. It also led to the widespread adoption of Model Checking by the computer hardware industry. For this invention, Bryant, Clarke, Emerson, and McMillan received the 1998 Paris Kanellakis Award for Theory and Practice from ACM. In 1999, they also received the Allen Newell Award for Research Excellence from Carnegie Mellon University. Sifakis, together with Thomas A. Henzinger and Sergio Yovine, extended the Model Checking approach to address verification of real time systems. In 2001, Sifakis received the Centre National de la Recherche Scientifique Silver Medal.
Edmund M. Clarke
Dr. Clarke is the FORE Systems Professor of Computer Science and Professor of Electrical and Computer Engineering at Carnegie Mellon University. He has served on the editorial boards of numerous journals and is the former editor-in-chief of Formal Methods in Systems Design. He is a co-founder with Robert Kurshan, Amir Pnueli, and Joseph Sifakis of the International Conference on Computer Aided Verification (CAV) and serves on the steering committee. He received a Technical Excellence Award from the Semiconductor Research Corporation in 1995, and the IEEE Harry M. Goode Memorial Award in 2004. He is a Fellow of ACM and the IEEE Computer Society, and was elected to the National Academy of Engineering in 2005. Dr. Clarke was awarded a B.A. degree in mathematics from the University of Virginia and a M.A. degree in mathematics from Duke University. He earned a Ph.D. degree in computer science from Cornell University, and has taught at Duke University and Harvard University.
E. Allen Emerson
Dr. Emerson is an Endowed Professor in Computer Sciences at the University of Texas at Austin. 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, including ACM Transactions on Computational Logic, Formal Aspects of Computing, and Formal Methods in Systems Design. He serves on the steering committee of the International Symposium on Automated Technology for Verification and Analysis (ATVA) as well as the International Conference on Verification, Model Checking, and Abstract Interpretation (VMCAI). Dr. Emerson received a B.S. degree in mathematics from University of Texas at Austin, and a Ph.D. in applied mathematics from Harvard University.
Joseph Sifakis
Dr. Sifakis is the founder of Verimag Laboratory, a leading research center for embedded systems in Grenoble, France, where he was director from 1993-2006. He is Research Director of Centre National de la Recherche Scientifique, and Director of the CARNOT Institute on Intelligent Software and Systems in Grenoble. Dr. Sifakis is a member of the editorial board of several journals, and the scientific coordinator of the Artist2 and ArtistDesign European Networks of Excellence on Embedded Systems Design. He is co-founder with Edmund Clarke, Robert Kurshan, and Amir Pnueli of the International Conference on Computer Aided Verification (CAV). He earned a degree in electrical engineering from the Technical University of Athens and a Ph.D. in computer science from the University of Grenoble.
ACM will present the Turing Award at the annual ACM Awards Banquet on June 21, 2008, in San Francisco, CA.
About the A.M. Turing Award
The A.M. Turing Award was named for Alan M. Turing, the British mathematician who articulated the mathematical foundation and limits of computing, and who was a key contributor to the Allied cryptanalysis of the German Enigma cipher during World War II. Since its inception in 1966, the Turing Award has honored the computer scientists and engineers who created the systems and underlying theoretical foundations that have propelled the information technology industry. For additional information, click on http://awards.acm.org/turing.
About ACM
ACM (www.acm.org) is widely recognized as the premier organization for computing professionals, delivering resources that advance the computing and IT disciplines, enable professional development, and promote policies and research that benefit society. ACM hosts the computing industry’s leading Digital Library and Portal to Computing Literature, and serves its global membership with journals and magazines, special interest groups, conferences, workshops, electronic forums, Career Resource Centre and Professional Development Centre.