NSF - National Science Foundation

Page Content   Main Menu   Local Links   Search   What is this view?

You are here: Home > News

News Release 08-022

Model Checking Pioneers Receive Turing Award, Most Prestigious in Computing

Researchers created technique used in range of everyday tasks

Image of a printed circuit similar to those used in modern electronics.

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."


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) 2017, its budget is $7.5 billion. NSF funds reach all 50 states through grants to nearly 2,000 colleges, universities and other institutions. Each year, NSF receives more than 48,000 competitive proposals for funding and makes about 12,000 new funding awards.

Get News Updates by Email

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

Main Links

Local Links

What is this view?

You are using a dynamic assistive view of the National Science Foundation site. It has all the same data and features of the original site but formatted just with assistive users in mind. It has links and content reorganized to aid assistive users and has controls at the bottom under assistive options that allow you to control key aspects such as font size and contrast colors etc.
This is not a separate text-only site, it's a dynamic view that uses unique technology from Usablenet to give assistive users better, more accessible access to the same content and features as all users that use the graphic view of the site.

Assistive Options

Top of page

Assistive Options

Open the original version of this page.

Usablenet Assistive is a Usablenet product. Usablenet Assistive Main Page.