NASA Logo, National Aeronautics and Space Administration
Intelligent Systems Division Banner

Rozier Authors “Nugget” on Value of Formal Methods for Safety-Critical System Verification

Theoretical Computer Science (TCS) Visions has completed a successful effort to produce a set of “nuggets” used for arguing for the importance of computing research to a variety of audiences. A nugget consists of a single slide with a title, tagline, and image that capture an area of theoretical computer science, accompanied by a written document containing a summary and rationale for the research area.

Kristin Y. Rozier served as the lead for the Life-Critical System Verification nugget and is the primary author of the description of the need for, and value of, formal methods for safety-critical system verification, as well as a contributor to other nuggets. Rozier also co-chaired the sub-group focusing on security, privacy, and reliability, helping to organize all nuggets in these areas. This project kicked off at the Visions for Theoretical Computer Science Workshop in 2008.

The nuggets have received very positive reactions from the Computing Community Consortium (CCC), the Defense Advanced Research Projects Agency (DARPA), and the National Science Foundation (NSF), and they may also appear in a future issue of the Communications for the Association of Computing Machinery (CACM) magazine. Jeannette Wing, the Assistant Director of NSF's Computer and Information Science and Engineering Directorate, said about the nuggets, “They are fantastic and the cover slides are gorgeous.” She praised the broad coverage and cutting-edge subject matter and said this work is “pushing the frontiers of computing by deepening the foundational understanding of our field, without losing sight of the potential broad impact on society.”

The completed TCS nuggets are available here.

BACKGROUND: Theoretical Computer Science (TCS) Visions, sponsored by the Computing Community Consortium (CCC) and the Special Interest Group for the Association of Computing Machinery (SIGACT) Committee for the advancement of theoretical computer science, aimed to accomplish two goals with the development of these nuggets:

  1. Identify broad research themes within theoretical computer science (TCS) that have potential for a major impact in the futur
  2. Distill these research directions into compelling “nuggets” that can quickly convey their importance to a layperson (such as science advisors for senators

The main purpose of these nuggets will be to help the CCC and others argue for the importance of computing research, and TCS in particular, to a variety of audiences. Some may also inspire the development of new centers or large-scale research activities (as might be funded by the new NSF Expeditions in Computing program), and others may be broadened and inspire entirely new programs (similar to the way the NSF Cyber-enabled Discovery and Innovation (CDI) program was inspired by ‘06-07 workshops on Computer Science as a Lens on the Sciences).

NASA PROGRAM FUNDING: Next Generation Air Transport System (NGATS) project

COLLABORATORS: This work has been completed in collaboration with thirty-two other researchers in theoretical computer science, from both academia and industry. The nuggets on security, privacy, and reliability were primarily designed in collaboration with Cynthia Dwork (Microsoft Research), Dick Lipton (Georgia Tech), Amit Sahai (UCLA), and Salil Vadhan (Harvard).

Contact: Kristin Y. Rozier

+NASA Home

+Ames Home

Rozier Authors “Nugget” on Value of Formal Methods for Safety-Critical System Verification
+ Home + Organization + News + Research Areas + Publications + Software + Internal Systems Help
First Gov logo
NASA Logo - nasa.gov