Continuous Integrated Invariant Inference

Award Information
Agency:
National Aeronautics and Space Administration
Branch
n/a
Amount:
$100,000.00
Award Year:
2011
Program:
SBIR
Phase:
Phase I
Contract:
NNX11CD03P
Award Id:
n/a
Agency Tracking Number:
105222
Solicitation Year:
2010
Solicitation Topic Code:
A1.14
Solicitation Number:
n/a
Small Business Information
531 Esty Street, Ithaca, NY, -
Hubzone Owned:
N
Minority Owned:
N
Woman Owned:
N
Duns:
603978321
Principal Investigator:
DavidCok
Principal Investigator
(607) 273-7340
dcok@grammatech.com
Business Contact:
PaulAnderson
Business Official
(607) 273-7340
paul@grammatech.com
Research Institute:
Stub




Abstract
The proposed project will develop a new technique for invariant inference and embed this and other current invariant inference and checking techniques in an easy-to-use tool. The result will enhance an engineer's ability to use formal methodsÂ? generating, editing, reviewing, proving and testing invariants Â? and improve productivity in verification and validation of safety and correctness properties software. Currently, invariants that represent such properties require extensive human effort to write; automated techniques, thoughimproving, are still insufficiently capable of automatically inferring them. The proposed project will develop innovative techniques to infer logical invariants describing the behavior of individual software modules by combining static (analyzing a program without running it) and hybrid analysis (inferring invariants from observations of executing software). In particular, the project will (a) combine concolic execution and hybrid analysis to find candidate invariants from high-branch-coverage test suites, (b) apply that combination to obtain invariants for individual functions and data structures, (c) iterate the analysis to broaden data coverage of the test suite and improve the accuracy of invariants, and (d) create early prototypes and development plans to integrate the resulting tools in selected IDEs (Eclipse and GrammaTech's CodeSonar tool). In carrying out this project, GrammaTech will build on its static analysis tools, concolic engine, and software dynamic translation module. It will leverage its base of research and expertise in static and hybrid analysis, specification languages, automated SMT theorem provers, and GUI tools for program analysis and development. The commercialization prospects for the proposed project are enhanced by GrammaTech's demonstrated experience in producing prototypes and commercial products from research results.

* 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