Formal Verification of Programming by Demonstration Systems

Award Information
Agency:
National Aeronautics and Space Administration
Branch
n/a
Amount:
$99,942.00
Award Year:
2011
Program:
SBIR
Phase:
Phase I
Contract:
NNX11CD50P
Award Id:
n/a
Agency Tracking Number:
104935
Solicitation Year:
2010
Solicitation Topic Code:
X6.01
Solicitation Number:
n/a
Small Business Information
421 Southwest Sixth Avenue, Suite 300, Portland, OR, 97204-1622
Hubzone Owned:
N
Minority Owned:
N
Woman Owned:
N
Duns:
098009918
Principal Investigator:
E. RoganCreswick
Principal Investigator
(503) 808-7195
creswick@galois.com
Business Contact:
Anne MarieMcClaran
Business Official
(503) 808-7203
anne@galois.com
Research Institute:
Stub




Abstract
Automated tools are quickly making inroads into casual computing environments, solving progressively more complex tasks. However, these advancements still require trading reliability for convenience. Frequent minor failures are acceptable in casual environments, but critical systems cannot make the same exchange. The software systems that NASA develops could greatly benefit from machine learning technologies that have been applied to casual computing, if the software developed by learning algorithms could be verified.We propose to apply formal methods to machine learning, and specifically Programming by Demonstration (PBD). The existing technology readiness level is very low: no known verifiable PBD systems have been deployed and the existing research in the area is limited. The Phase I effort will result inpublications and a prototype implementation of a verifiable PBD system using SMT solvers. Phase II will build on Phase I publications and prototypes to demonstrate increased verification capabilities through the application of more complex formal methods, such as model checking. Verifiable machine learning would allow for trainable systems that meet critical properties, but are still adaptable to specific use cases. Such tools could be re-purposed for multiple applications without incurring the development costs associated with manual automation techniques today.

* information listed above is at the time of submission.

Agency Micro-sites


SBA logo

Department of Agriculture logo

Department of Commerce logo

Department of Defense logo

Department of Education logo

Department of Energy logo

Department of Health and Human Services logo

Department of Homeland Security logo

Department of Transportation logo

Enviromental Protection Agency logo

National Aeronautics and Space Administration logo

National Science Foundation logo
US Flag An Official Website of the United States Government