Description
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.