SHF: Small: Measurable Program Analysis

软件无处不在，它的正确运行在社会的健康、生产力和安全以及个人的生活中发挥着越来越重要的作用。因此，需要能够经济有效地测量软件正确性的技术，以建立良好的基础来判断软件是否准备好部署和广泛使用。这些措施的可获得性为平衡使用软件系统的回报与其失败的风险提供了证据基础。这种类型的证据有可能改变软件消费者的期望，并增强他们对软件行为的理解，以及如何将他们的信任置于该行为中。正确性的证据对安全关键软件具有明显的价值，但更广泛地说，它将有助于塑造社会将软件视为关键基础设施的方式，以及它对制造商期望的专业性。该项目将数十年来基于抽象的程序分析和符号执行工作的结果与最近量化逻辑公式解空间的结果相结合。该项目探索了可扩展的非定量分析的新颖组合和阶段，以识别可能错误的程序行为的子空间，然后重点对这些子空间进行量化分析。这为可测量程序分析(MPA)提供了一种方法，在保证可伸缩性的同时产生安全和准确的结果。该项目产生了实现各种MPA的理论和工具，对这些分析的成本和收益进行了实证评估，并与研究社区公开分享了所有结果和产物。

Software is everywhere and its correct operation plays an increasingly important role in the health, productivity, and safety of society and in the lives of individuals. Consequently, there is a need for techniques that can cost-effectively measure software correctness to establish a well-founded basis for making judgments about whether software is ready for deployment and wide spread use. The availability of such measures provides an evidentiary basis for balancing the rewards of using a software system against the risks of its failure. This type of evidence has the potential to transform the expectations of consumers of software and to enhance their understanding of software behavior and how to place their trust in that behavior. Evidence of correctness has obvious value for safety critical software, but more broadly it will help shape how society views software as critical infrastructure and the professionalism that it expects of its manufacture.This project blends the outcomes of decades of work on abstraction-based program analysis and symbolic execution with recent results in quantifying the solution space of a logical formula. The project explores novel combinations and staging of scalable non-quantitative analyses, to identify sub-spaces of program behavior that may be erroneous, followed by quantitative analyses focused on those sub-spaces. This offers an approach to measurable program analysis (MPA) that promises scalability while yielding safe and accurate results. The project produces theory and tools that realize a variety of MPA, empirically evaluates the cost and benefit of these analyses, and openly shares all results and artifacts with the research community.