Collaborative Research: SHF: Small: A General Framework for Responsive Static Analysis

社会越来越依赖软件的可靠性和安全性。 抽象解释是一种行之有效的方法，用于证明软件没有某些类型的错误。 然而，对于工业规模的软件，标准的抽象解释技术可能需要几个小时才能完成，这使得它们难以集成到现代软件开发实践中。 这个项目开发了一个响应式静态分析框架，它保留了抽象解释的能力，同时在常见用例中运行得更快。 该项目的新颖之处是用于响应地运行抽象解释的新算法，相应的数学证明这些算法产生所需的正确结果，以及算法的工作实现。 该项目的影响是更大的性能和适用性的强大的抽象解释技术验证软件的正确性，这反过来又会产生更可靠和安全的software.The项目建立在一个最近开发的框架要求抽象解释，需求驱动和增量分析方法的基础上具体化的分析计算和依赖关系的图形结构。通过这种方法的推广，该项目将扩展框架来处理组合分析，这对于过程调用的有效分析和基于细化的分析至关重要，以实现具有不同精度和可扩展性的组合分析。这种广义的框架将促进从头开始的一致性，响应分析的一个重要属性的可证明的保证。该项目还将实施通用框架，并将其与具有挑战性的分析问题实例化，解决研究挑战，使框架practices.This奖项反映了NSF的法定使命，并已被认为是值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估的支持。

Society increasingly relies on the reliability and security of software. Abstract interpretation is a well-established methodology for proving that software is free of certain classes of bugs. However, for industrial-scale software, standard abstract interpretation techniques may take hours to complete, making them difficult to integrate into modern software development practices. This project develops a framework for responsive static analysis, which retains the power of abstract interpretation while running much more quickly for common use cases. The project's novelties are new algorithms for running abstract interpretation responsively, corresponding mathematical proofs that these algorithms produce the desired, correct results, and working implementations of the algorithms. The project's impacts are greater performance and applicability of powerful abstract interpretation techniques for verifying software correctness, which in turn will yield more reliable and secure software.The project builds on a recently-developed framework for demanded abstract interpretation, a demand-driven and incremental analysis approach based on reifying analysis computations and dependencies in a graph structure. Via generalizations of this approach, this project will extend the framework to handle compositional analysis, essential for efficient analysis of procedure calls, and refinement-based analysis, to enable combining analyses with varying levels of precision and scalability. This generalized framework will facilitate provable guarantees of from-scratch consistency, a crucial property for responsive analysis. The project will also implement the generalized framework and instantiate it with challenging analysis problems, addressing research challenges in making the framework practical.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.