Mathematically Rigorous Methods for Determining Software Quality Navy STTR FY2010.A Sol No.: Navy STTR FY2010.A Topic No.: N10A-T035 Topic Title: Mathematically Rigorous Methods for Determining Software Quality Proposal No.: N10A-035-0312 Firm: MZA Associates Corporation 2021 Girard Blvd. SE Suite 150 Albuquerque, New Mexico 87106-3140 Contact: DeLesley Hutchins Phone: (505) 245-9970 Web Site: http://mza.com 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. Benefits: The commercial development of the proposed framework will proceed in three phases. First, MZA is currently working on mission-critical software for laser weapons systems, and thus has an immediate need for a mathematically rigorous validation tool. Once the framework has proved itself in internal use, MZA will proceed to the second phase, and market it to other defense contractors and government organizations with similar needs. In the third phase, MZA plans to release the framework to the broader software industry as a commercial tool for formal software verification. The proposed framework has a number of capabilities that no other tool possesses, and should thus have a bright future as a commercial product. Return