News Release 08-022
Model Checking Pioneers Receive Turing Award, Most Prestigious in Computing
Researchers created technique used in range of everyday tasks
Model checking has helped create advanced devices that we depend on in our day-to-day lives.
February 8, 2008
This material is available primarily for archival purposes. Telephone numbers or other contact information may be out of date; please see current contact information at media contacts.
Officials from the National Science Foundation's (NSF) Computer and Information Science and Engineering (CISE) directorate cheered this week's announcement that Edmund M. Clarke, E. Allen Emerson and Joseph Sifakis have won the 2007 A.M. Turing Award, frequently referred to as the ‘Nobel Prize' of computing for their work on model checking. Clarke and Emerson have received funding and support from NSF throughout their distinguished careers.
Clarke, a computer science professor at Carnegie Mellon University and Emerson, a professor of computer science at the University of Texas, collaborated on much of this research, and they share the award with Sifakis, who worked independently at the University of Grenoble in France.
Presented by the Association for Computing Machinery, the A.M. Turing Award is named for the British mathematician Alan M. Turing. It is generally acknowledged as the most prestigious award in computing.
"NSF should be proud of its support of this research and the enormous impact it has had," said Jeannette Wing, assistant director for CISE.
Model checking plays an important role in almost all modern computers and computer-aided devices and systems. Modern life depends on these technologies for everything from personal computers and elevators in office buildings to life-support equipment in operating rooms. These systems must be dependable because they are so crucial to our day-to-day lives. As computer hardware and software became more complex over the past 30 years, their designers and manufacturers' needed new methods to verify that these devices and systems would perform as intended. Model checking provides a fast and automatic verification technique that uses algorithms and data structures to confirm the dependability of these systems.
"Model checking is a fast, automatic verification technique that is simple to teach and to learn," Wing said. "It has been applied to systems from a diverse range of sectors from telecommunications, to healthcare, to automobiles, to avionics, to security."
What makes model checking a tool of choice is that it produces what are known as ‘counterexamples' telling developers where they have potential errors in their designs. These counterexamples make it easier for computer hardware and software designers to debug their designs, which in turn cuts down on the time and costs associated with designing new systems.
The wide-spread adoption of model checking in modern computing and the recognition of Clarke, Emerson and Sifakis is an example of how NSF has supported cutting-edge research that eventually impacts society at large.
"NSF has supported research in model checking since its inception in the early 1980s, through its breakthrough research in the 1990s transforming how hardware companies change the way they verify chip and protocol designs, and more recently in the 2000s transforming how even software companies are debugging their code," Wing said. "Model checking has had and will continue to have enormous impact in the future-especially as our computing and information technology systems get more and more complex and as our society relies more and more on these complex systems for our daily lives."
-NSF-
Media Contacts
Dana W. Cruikshank, NSF, (703) 292-8070, email: dcruiksh@nsf.gov
Related Websites
More information about the Turing Award: http://awards.acm.org/homepage.cfm?srt=all&awd=140
The U.S. National Science Foundation propels the nation forward by advancing fundamental research in all fields of science and engineering. NSF supports research and people by providing facilities, instruments and funding to support their ingenuity and sustain the U.S. as a global leader in research and innovation. With a fiscal year 2023 budget of $9.5 billion, NSF funds reach all 50 states through grants to nearly 2,000 colleges, universities and institutions. Each year, NSF receives more than 40,000 competitive proposals and makes about 11,000 new awards. Those awards include support for cooperative research with industry, Arctic and Antarctic research and operations, and U.S. participation in international scientific efforts.
Connect with us online
NSF website: nsf.gov
NSF News: nsf.gov/news
For News Media: nsf.gov/news/newsroom
Statistics: nsf.gov/statistics/
Awards database: nsf.gov/awardsearch/
Follow us on social
Twitter: twitter.com/NSF
Facebook: facebook.com/US.NSF
Instagram: instagram.com/nsfgov