CAREER: Program Analysis with Precise Abstractions

程序分析技术是对程序行为的解释，在软件测试、bug发现和质量保证中得到了广泛的应用。一般来说，静态程序分析的问题是无法确定的。实际的程序分析通常通过不精确的抽象来过度逼近程序语义。本项目将基于图论设计精确的程序抽象，使程序分析技术更加可靠和可用。该项目的新颖之处在于(1)提供了精确抽象的统一理论，可用于设计具有形式化保证的更具原则性的分析技术；(2)为解决新兴领域的实际分析问题提供了更具可扩展性的程序分析框架。该项目的影响是(1)增加构建可靠软件的能力，(2)导致更可靠和可用的程序分析框架，用于分析软件工件，以及(3)倡导计算中抽象的基本概念。这个项目的目标是探索围绕着InterDyck图形抽象的理论发展和实践技术。它着重于开发一个系统的框架来精确地建模程序语义，并设计实用的算法来解决基于InterDyck图抽象的可达性问题。本项目主要探索三个方向：(1)理解InterDyck图形抽象的表达性和局限性；(2)开发高效的需求驱动和详尽的跨区可达性分析算法；(3)推广基于图抽象的程序分析综合教学方法。如果成功，该项目将显著提高我们对软件的推理能力，这对于我们社会所依赖的软件可靠性至关重要。此外，综合研究和教育活动将促进可靠软件的建设。该奖项反映了美国国家科学基金会的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。

Program analysis techniques reason about program behavior and have been widely used in software testing, bug finding, and quality assurance. In general, the problem of static program analysis is undecidable. Practical program analyses typically over-approximate program semantics via imprecise abstractions. This project will devise precise program abstractions based on graph theory to make program analysis techniques more reliable and usable. The project's novelties are (1) providing a unified theory of precise abstractions that can be used to design more principled analysis techniques with formal guarantees and (2) enabling more scalable program analysis frameworks for tackling practical analysis problems in emerging areas. The project's impacts are (1) increasing the capability of building reliable software, (2) leading to more reliable and usable program analysis frameworks for analyzing software artifacts, and (3) advocating the fundamental concept of abstraction in computing.The goal of this project is to explore theoretical developments and practical techniques centered around the InterDyck graph abstraction. It focuses on developing a systematic framework to precisely model program semantics and devise practical algorithms for solving the reachability problem based on the InterDyck graph abstraction. This project explores three main directions: (1) understanding the expressiveness and limitations of the InterDyck graph abstraction; (2) developing efficient demand-driven and exhaustive analysis algorithms for InterDyck-reachability; and (3) promoting an integrated educational approach to teach program analysis based on graph abstractions. If successful, the project will significantly enhance our ability to reason about software, which is vital for the software reliability upon which our society depends. Furthermore, the integrated research and education activities will facilitate the construction of 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.