CAREER: Foundations for Usable Program Analysis

软件几乎渗透到现代世界的方方面面，使软件可靠性成为一个巨大的、日益增长的社会问题。自动化程序分析和验证技术旨在以最小的开发人员努力提高可靠性，为软件开发人员提供工具来回答有关其代码行为的问题。由于几乎所有这样的问题都是无法确定的，过去50年来程序分析技术的进步一直是由启发式推理技术推动的。这些启发式方法在实践中通常是有效的，但它们可能很脆弱，并表现出违反直觉的行为，使得程序分析器难以使用。这个项目研究的问题是：如何定义软件开发人员可以理解和更改其行为的程序分析工具？该项目为可用的程序分析工具奠定了基础，以便提供软件开发人员可能依赖的行为和性能保证。它回顾了三个核心程序分析任务--数值不变量生成、终止分析和形状分析--并开发了可靠的推理原则来取代启发式。该项目贡献了新的程序分析算法和新的自动定理证明技术来支持这些分析。通过提高可用性，该项目旨在扩大程序分析的范围和影响，最终目标是创建更好、更可靠的软件。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

Software pervades almost every aspect of the modern world, making software reliability a large and growing societal concern. Automated program-analysis and -verification technology aims to increase reliability, with minimal developer effort, by providing software developers with tools to answer questions about the behavior of their code. Since nearly all such questions are undecidable, progress in program-analysis technology over the last fifty years has been driven by heuristic reasoning techniques. These heuristics are often effective in practice, but they can be brittle and exhibit counter-intuitive behavior, making program analyzers to difficult to use. This project investigates the question: how can program-analysis tools be defined whose behavior can be understood and altered by software developers?This project builds foundations for usable program-analysis tools in order to deliver behavioral and performance guarantees that software developers may rely upon. It revisits three core program-analysis tasks -- numerical-invariant generation, termination analysis, and shape analysis -- and develops dependable reasoning principles to replace heuristics. The project contributes new program-analysis algorithms and new automated theorem-proving technology to support these analyses. By improving usability, the project aims to increase the scope and impact of program analysis, with the ultimate goal of creating better, more reliable software.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.