Analysis-based verification: A programmer-oriented approach to the assurance of mechanical program properties

There is a constant and insidious loss of design intent throughout the software lifecycle. Developers make design decisions but fail to record these decisions or their rationale. As a consequence, quality and maintainability of software suffer, since additional effort must be expended to recover---and verify---lost design intent prior to implementing even minor changes in the code. This is particularly challenging for concurrent code. Our vision is to capture and verify critical design intent through the use of fragmentary specifications supported by targeted verification tools that can function alongside debugging and testing tools in the practitioner's toolkit for software quality and maintainability.;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 verification and bug finding on full-scale production code.