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.