权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

CAREER: Foundations for Usable Program Analysis

职业：可用程序分析的基础

基本信息

批准号：
1942537
负责人：
Zachary Kincaid
金额：
$ 60.71万
依托单位：
Princeton University
依托单位国家：
美国
项目类别：
Continuing Grant
财政年份：
2020
资助国家：
美国
起止时间：
2020-06-01 至 2025-05-31
项目状态：
未结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1942537&HistoricalAwards=false
关键词：
CAREER Foundations Usable Program Analysis

项目摘要

Software pervades almost every aspect of the modern world, making software reliability a large and growing societal concern. Automated program-analysis and -verification technology aims to increase reliability, with minimal developer effort, by providing software developers with tools to answer questions about the behavior of their code. Since nearly all such questions are undecidable, progress in program-analysis technology over the last fifty years has been driven by heuristic reasoning techniques. These heuristics are often effective in practice, but they can be brittle and exhibit counter-intuitive behavior, making program analyzers to difficult to use. This project investigates the question: how can program-analysis tools be defined whose behavior can be understood and altered by software developers?This project builds foundations for usable program-analysis tools in order to deliver behavioral and performance guarantees that software developers may rely upon. It revisits three core program-analysis tasks -- numerical-invariant generation, termination analysis, and shape analysis -- and develops dependable reasoning principles to replace heuristics. The project contributes new program-analysis algorithms and new automated theorem-proving technology to support these analyses. By improving usability, the project aims to increase the scope and impact of program analysis, with the ultimate goal of creating better, more 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.

软件几乎渗透到现代世界的每一个方面，使软件可靠性成为一个巨大的和日益增长的社会问题。自动程序分析和验证技术旨在通过为软件开发人员提供工具来回答有关其代码行为的问题，从而以最小的开发人员努力来提高可靠性。由于几乎所有这些问题都是不可判定的，过去50年来程序分析技术的进步一直是由启发式推理技术推动的。这些方法在实践中通常是有效的，但它们可能很脆弱，并表现出违反直觉的行为，使程序分析器难以使用。这个项目研究的问题是：如何定义程序分析工具，其行为可以被软件开发人员理解和修改？该项目为可用的程序分析工具奠定了基础，以提供软件开发人员可能依赖的行为和性能保证。它重新审视了三个核心的程序分析任务--数值不变式生成、终止分析和形状分析--并开发了可靠的推理原则来取代逻辑分析。该项目贡献了新的程序分析算法和新的自动定理证明技术来支持这些分析。通过提高可用性，该项目旨在扩大程序分析的范围和影响，最终目标是创建更好、更可靠的软件。该奖项反映了NSF的法定使命，并通过使用基金会的知识价值和更广泛的影响审查标准进行评估，被认为值得支持。