SHF: Small: Measurable Program Analysis

SHF：小型：可衡量的计划分析

• 批准号: 1901769
• 负责人: Matthew Dwyer
• 金额: $ 21.97万
• 依托单位: University of Virginia Main Campus
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2018
• 资助国家: 美国
• 起止时间: 2018-08-11 至 2020-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1901769&HistoricalAwards=false
• 关键词: SHF; Small; Measurable; Program; Analysis

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.

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