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.