Continuous Integrated Invariant Inference

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, though improving, 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.

The project expects to market a commercial version of the tools it generates first to existing GrammaTech customers, particularly with early adopter releases. The most relevant application areas are safety-critical and correctness-critical software: software for medical devices, commercial avionics, automotive systems, and other embedded software. The capability to operate on machine code without source code will be useful for customers needing reverse engineering or security analysis tools. The tool's test generation capabilities will also be attractive to desktop software manufacturers that may not be interested in verification of software properties. GrammaTech will enlist some current customers as early adopters. Among its active customers are facilities whose task is software inspection and certification; the company expects that these will be natural reviewers and customers for the project's technology. The project anticipates that placing the new technology in existing IDEs will smooth the path to initial experimentation and eventual adoption of the new technology.

The project will target NASA activities concerned with verification and validation, safety-critical avionics (including the NextGen air traffic control system), and with assessment of COTS or third party software to be included in critical systems. GrammaTech will seek reviews and early adopters of the developed technology among the company's current customers of its existing products in several of NASA's facilities. For example, GrammaTech has worked closely with the LaRS group at JPL in developing other product enhancements and would solicit their review of this new technology; in addition, GrammaTech's static analysis tools are in current use in NASA's V&V facilities.

This is early/mid-stage (TRL 5) — the most realistic path in is NASA SBIR/STTR, which funds small businesses and research institutions to develop technology aligned with NASA's needs (equity-free, phased funding). Check whether a current SBIR/STTR solicitation topic overlaps with this project's technology area, or contact the project directly (above) to ask.

None of these are guaranteed paths for this specific project — TechPort itself doesn't have an "apply" button. Reaching out to the contact(s) above with a specific question is usually the fastest way to find out what's actually open.