CAREER: Program Analysis with Precise Abstractions

职业：精确抽象的程序分析

• 批准号: 2237440
• 负责人: Qirun Zhang
• 金额: $ 52.5万
• 依托单位: Georgia Tech Research Corporation
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-07-01 至 2028-06-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2237440&HistoricalAwards=false
• 关键词: CAREER; Program; Analysis; Precise; Abstractions

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.

程序分析技术有关程序行为的原因，并已广泛用于软件测试，错误查找和质量保证。通常，静态程序分析的问题是不可确定的。实用程序分析通常通过不精确的抽象来过度陈述的程序语义。该项目将基于图理论设计精确的程序摘要，以使程序分析技术更加可靠和可用。该项目的新颖性是（1）提供统一的精确抽象理论，可用于设计具有正式保证的更多原则性分析技术，以及（2）启用更可扩展的程序分析框架，以解决新兴领域中的实际分析问题。该项目的影响是（1）提高构建可靠软件的能力，（2）导致更可靠且可用的程序分析框架用于分析软件工件，以及（3）提倡在计算机中抽象的基本概念。该项目的目的是探索围绕围绕Interdyck的理论发展和实践技术。它着重于开发一个系统的框架来精确模拟程序语义，并设计了基于Interdyck图形抽象的可及性问题的实用算法。该项目探讨了三个主要方向：（1）理解相互作用图形抽象的表现力和局限性； （2）开发有效的需求驱动和详尽的分析算法，以实现相互影响的性能； （3）促进一种基于图形摘要的综合教育方法来教授程序分析。如果成功，该项目将显着增强我们对软件的推理能力，这对于我们社会依赖的软件可靠性至关重要。此外，综合的研究和教育活动将有助于构建可靠的软件。该奖项反映了NSF的法定任务，并且使用基金会的知识分子优点和更广泛的影响审查标准，被认为值得通过评估来获得支持。