CAREER: Abstracting Programs for Automated Debugging

调试是软件开发中最耗时的方面之一，每年要花费数十亿美元。任何减少调试中涉及的手工工作的自动化都可以对软件生产力产生重大影响。故障定位是所有调试活动的一个组成部分。一旦在程序中发现了不期望的行为，就必须在开发修复之前确定实际的缺陷。大多数现有的故障定位技术依赖于高质量测试套件的可用性，这限制了它们的适用性。一个有希望的替代方案是静态分析有缺陷的程序片段而不依赖于测试的技术。该项目的目标是开发实用的静态故障定位算法。如果这样的算法是可用的，它们将扩大程序的范围，使自动调试工具可以应用，并且能够创建具有改变软件开发和维护方式的潜力的新工具。本课题的主要研究假设是能够实现实用的静态故障定位算法。为了验证这一假设，PI将探索保守地过度近似错误程序行为的抽象。这些抽象的精确性必须是有针对性的，这样才能保留程序中与错误相关的部分，并精确地识别缺陷。这种目标抽象的构建可以自动化的假设得到了故障定位和形式化验证之间存在联系的观察的支持。拟议的工作将探索利用这种联系的新技术和算法。这些算法将在静态故障定位工具中实现和评估，该工具将作为研究高级自动化调试技术的工具。

Debugging is one of the most time consuming aspects of software development costing the economy billions of dollars annually. Any automation that reduces the manual effort involved in debugging can have a significant impact on software productivity. An integral part of all debugging activities is the task of fault localization. Once undesired behavior is spotted in a program, the actual defect has to be identified before a fix can be developed. Most existing fault localization techniques rely on the availability of high quality test suites, which limits their applicability. One promising alternative is techniques that statically analyze the faulty program fragment and do not rely on testing. The goal of this project is to develop practical static fault localization algorithms. If such algorithms were available, they would broaden the scope of programs to which automated debugging tools can be applied and enable the creation of novel tools that have the potential to change the way in which software is developed and maintained.The main research hypothesis of this project is that practical static fault localization algorithms can be realized. To validate this hypothesis the PI will explore abstractions that conservatively over-approximate the behavior of faulty programs. The precision of these abstractions must be targeted so that the error-relevant portions of the program are preserved and the defect is precisely identified. The hypothesis that the construction of such targeted abstractions can be automated is supported by the observation that there exists a connection between fault localization and formal verification. The proposed work will explore new techniques and algorithms that leverage this connection. These algorithms will be implemented and evaluated in a static fault localization tool that will serve as a vehicle for studying advanced automated debugging techniques.