SBIR-STTR Award

Mathematically Rigorous Methods for Determining Software Quality
Award last edited on: 5/10/2019

Sponsored Program
STTR
Awarding Agency
DOD : Navy
Total Award Amount
$69,981
Award Phase
1
Solicitation Topic Code
N10A-T035
Principal Investigator
Delesley Hutchins

Company Information

MZA Associates Corporation

4900 Lang Avenue NE Suite 100
Albuquerque, NM 87109
   (505) 245-9970
   abq.info@mza.com
   www.mza.com

Research Institution

University of California - Santa Cruz

Phase I

Contract Number: N00014-10-M-0250
Start Date: 6/28/2010    Completed: 4/30/2011
Phase I year
2010
Phase I Amount
$69,981
Current software development and testing methodologies are inadequate for validating software in mission-critical applications. As Dijstra famously stated: "testing can be used to show the presence of bugs, but never to show their absence." When lives and national security is at stake, there is a need for mathematically rigorous techniques that can verify the absence of bugs. We propose to develop a framework for software verification and validation using the technique of type-based static analysis. Type theory, and static analysis using types, has been extensively studied in the academic literature, but most of that research has not yet been used to build real-world tools for software verification. Type-based static analysis is both powerful and mathematically rigorous, and offers significant advantages in terms of scalability and modularity over competing techniques. Our proposed framework will be capable of analyzing code written in C, C++, Java, C#, and other languages, and will be able to analyze both source code and compiled binaries. The framework will use automatic type inference to derive appropriate safety properties for common programming patterns, but will also allow the user to supply annotations that guide the analysis algorithms when proving more difficult properties.

Keywords:
Software Security, Software Security, Mission Critical Code, , Model Checking, Formal Proofs, Memory Safety, Software Verification, Type Based Static Analysis, Race Conditions

Phase II

Contract Number: ----------
Start Date: 00/00/00    Completed: 00/00/00
Phase II year
----
Phase II Amount
----