USA flag logo/image

An Official Website of the United States Government

Mathematically Rigorous Methods for Determining Software Quality

Award Information

Agency:
Department of Defense 		Branch:
Navy 		Award ID:
95158 		Program Year/Program:
2010 / STTR
Agency Tracking Number:
N10A-035-0312 		Solicitation Year:
N/A 		Solicitation Topic Code:
NAVY 10T035 		Solicitation Number:
N/A
Small Business Information
MZA Associates Corporation
2021 Girard SE Suite 150 Albuquerque, NM -
View profile »
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No
 
Phase 1
Fiscal Year: 2010
Title: Mathematically Rigorous Methods for Determining Software Quality
Agency / Branch: DOD / NAVY
Contract: N00014-10-M-0250
Award Amount: $69,981.00
 

Abstract:

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.

Principal Investigator:

DeLesley Hutchins
Senior Software Engineer
5052459970
Delesley.Hutchins@mza.com

Business Contact:

Robert Praus
President
5052459970
Robert.Praus@mza.com
Small Business Information at Submission:

MZA Associates Corporation
2021 Girard SE Suite 150 Albuquerque, NM 87106

EIN/Tax ID: 850400557
DUNS: N/A
Number of Employees:
Woman-Owned: No
Minority-Owned: No
HUBZone-Owned: No
Research Institution Information:
University of California Santa Cruz
1156 High Street
Santa Cruz, CA 95064
Contact: Cormac Flanagan
Contact Phone: 8314595375