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.