Program analysis tools are starting to change how software is developed. Verifiers can now eliminate certain complex bugs in large code bases, and automatic refactoring tools can greatly simplify code cleanup. Nevertheless, writing robust large-scale software remains a challenge, as greater use of component frameworks complicates debugging and program understanding. Developers need more powerful programming tools to combat this complexity and produce reliable code.
This dissertation presents two techniques for more powerful debugging and program understanding tools based on refinement. In general, refinement-based techniques aim to discover interesting properties of a large program by only reasoning about the most important parts of the program (typically a small amount of code) precisely, abstracting away the behavior of much of the program. Our key contribution is the first framework for effective refinement-based handling of object-oriented data structures; pervasive use of such data structures thwarts the effectiveness of most existing analyses and tools.
Our two refinement-based techniques significantly advance the state-of-the-art in program analyses and tools for object-oriented languages. The first technique is a refinement-based points-to analysis that can compute precise answers in interactive time. This analysis enables precise reasoning about data structure behavior in clients that require interactive performance, e.g., just-in-time compilers and interactive development environment (IDE) tools. Our second technique is thin slicing, which gives usable answers to code relevance questions -- e.g., "What code might have caused this crash?" -- addressing a long-standing challenge for analysis tools. In this dissertation, we describe the design and implementation of these techniques and present experimental evaluations that validate their key properties.
Researchers may make free and open use of the UC Berkeley Library’s digitized public domain materials. However, some materials in our online collections may be protected by U.S. copyright law (Title 17, U.S.C.). Use or reproduction of materials protected by copyright beyond that allowed by fair use (Title 17, U.S.C. § 107) requires permission from the copyright owners. The use or reproduction of some materials may also be restricted by terms of University of California gift or purchase agreements, privacy and publicity rights, or trademark law. Responsibility for determining rights status and permissibility of any use or reproduction rests exclusively with the researcher. To learn more or make inquiries, please see our permissions policies (https://www.lib.berkeley.edu/about/permissions-policies).