CAREER: Program Analysis with Precise Abstractions

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

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.