Software is everywhere and its correct operation plays an increasingly important role in the health, productivity, and safety of society and in the lives of individuals. Consequently, there is a need for techniques that can cost-effectively measure software correctness to establish a well-founded basis for making judgments about whether software is ready for deployment and wide spread use. The availability of such measures provides an evidentiary basis for balancing the rewards of using a software system against the risks of its failure. This type of evidence has the potential to transform the expectations of consumers of software and to enhance their understanding of software behavior and how to place their trust in that behavior. Evidence of correctness has obvious value for safety critical software, but more broadly it will help shape how society views software as critical infrastructure and the professionalism that it expects of its manufacture.
This project blends the outcomes of decades of work on abstraction-based program analysis and symbolic execution with recent results in quantifying the solution space of a logical formula. The project explores novel combinations and staging of scalable non-quantitative analyses, to identify sub-spaces of program behavior that may be erroneous, followed by quantitative analyses focused on those sub-spaces. This offers an approach to measurable program analysis (MPA) that promises scalability while yielding safe and accurate results. The project produces theory and tools that realize a variety of MPA, empirically evaluates the cost and benefit of these analyses, and openly shares all results and artifacts with the research community.
