Institute for Software Research
School of Computer Science, Carnegie Mellon University
Analysis-Based Verification: A Programmer-Oriented Approach
Timothy J. Hallaron
This thesis advances the idea of focused analysis-based verification as a scalable and adoptable approach to the verification of mechanical program properties. The main contribution of the research is the development of the concept of sound combined analyses, through which results of diverse low-level program analyses can be combined in a sound way to yield results of interest to software developers.The contribution includes the underlying logic of combined analysis, the design of the user experience and tool engineering approach, and field validation on diverse commercial and open source code bases. Building on prior work in semantic program analysis, this approach enables sound tool-supported verification of nontrivial narrowly-focused mechanical properties about programs with respect to explicit models of design intent. These models are typically expressed as code annotations, and can be used even when adopted late in the software lifecycle for real-world systems.
In addition to providing a sound approach to combining fragmentary analysis results, the logic can support abductive inference of additional fragments of design intent. The proposed fragments that are deemed valid by the software developer can then be verified for consistency with code using an automated tool. The soundness of the logic for combined analysis is proved using an intuitionistic natural deduction calculus and other techniques. We validate our approach through the 9 field trials of a prototype tool that verifies properties related to multithreading and race conditions on a diverse sample of commercial, open source, and government code. In the majority of the field trials, this validation process included direct use of the prototype tool by disinterested professional developers and demonstrated that the tool performs useful verication and bug finding on full-scale production code.