Title: Alternating Conditional Analysis
Abstract: Program analysis tools typically compute either "may" or "must" information. By accumulating both kinds of information computed with respect to different portions of a program’s state space, it is possible to collect a comprehensive view of how program inputs relate to some property. We do so by introducing the framework of an alternating conditional analysis, which computes a sound characterization of all the ways a program either may or must satisfy some property. This is computed by alternating between over- and underapproximate analyses, conditioning analyses to ignore portions of the program that have already been analyzed, and combining the results of state-of-the-art analysis tools in a portfolio run in parallel. The characterization can be used to facilitate software engineering tasks ranging from fault localization and repair to quantitative program analysis for reliability.
Committee Members: Matthew Dwyer (Advisor), Mary Lou Soffa, Sebastian Elbaum, Homa Alemzadeh, ThanhVu Nguyen