Press 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. Credit and Larger Version

February 8, 2008

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 dcruiksh@nsf.gov

Related Websites
More information about the Turing Award: http://awards.acm.org/homepage.cfm?srt=all&awd=140

The National Science Foundation (NSF) is an independent federal agency that supports fundamental research and education across all fields of science and engineering. In fiscal year (FY) 2009, its budget is $9.5 billion, which includes $3.0 billion provided through the American Recovery and Reinvestment Act. NSF funds reach all 50 states through grants to over 1,900 universities and institutions. Each year, NSF receives about 44,400 competitive requests for funding, and makes over 11,500 new funding awards. NSF also awards over $400 million in professional and service contracts yearly.

 Get News Updates by Email 

Useful NSF Web Sites:
NSF Home Page: http://www.nsf.gov
NSF News: http://www.nsf.gov/news/
For the News Media: http://www.nsf.gov/news/newsroom.jsp
Science and Engineering Statistics: http://www.nsf.gov/statistics/
Awards Searches: http://www.nsf.gov/awardsearch/