Collaborative Research: SHF: Medium: Efficient and Trustworthy Proof Engineering

合作研究：SHF：中：高效且值得信赖的证明工程

基本信息

批准号：
2107291
负责人：
Milos Gligoric
金额：
$ 54万
依托单位：
University of Texas at Austin
依托单位国家：
美国
项目类别：
Continuing Grant
财政年份：
2021
资助国家：
美国
起止时间：
2021-05-01 至 2025-04-30
项目状态：
未结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=2107291&HistoricalAwards=false
关键词：
Collaborative Research SHF Medium Efficient

项目摘要

Formal verification of software in a proof assistant (such as Coq) can establish the correctness of software, preventing software bugs that could otherwise lead to significant financial losses or even loss of life. Unfortunately, proof assistants are not currently well adapted to large-scale software development and are expensive to use in terms of both development time and expertise. The goal of this project is to increase productivity of proof engineers (i.e., users of proof assistants) via techniques that simplify development and maintenance of large verification projects, as well as to increase trustworthiness in the toolchain commonly used by proof engineers. The project's novelties include learning-based and analytical approaches for proof construction, extraction, and maintenance, as well as testing techniques for establishing the trustworthiness of proof assistants. The project's impacts are increased productivity and increased software quality.This project develops techniques that help proof engineers (1) construct proofs by learning and enforcing conventions, automatically locating relevant lemmas, and synthesizing generalized invariants; (2) augment the extraction of executable code from verified artifacts with runtime monitoring for checking assumption violations and with novel support for generating executable variants of logical specifications; and (3) facilitate the maintenance of large proof repositories by detecting brittle proof scripts, as well as learning common transformations. Furthermore, to increase trust in the proof engineering toolchain, the investigators develop testing techniques that target the core components of proof assistants.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.

在证明助手（例如 Coq）中对软件进行形式化验证可以确定软件的正确性，防止软件错误，否则可能导致重大财务损失甚至生命损失。不幸的是，证明助手目前还不能很好地适应大规模软件开发，并且在开发时间和专业知识方面使用起来都很昂贵。该项目的目标是通过简化大型验证项目的开发和维护的技术来提高证明工程师（即证明助手的用户）的生产力，并提高证明工程师常用的工具链的可信度。该项目的新颖之处包括用于证明构建、提取和维护的基于学习和分析的方法，以及用于建立证明助手可信度的测试技术。该项目的影响是提高生产力和提高软件质量。该项目开发的技术可帮助证明工程师（1）通过学习和执行约定、自动定位相关引理以及综合广义不变量来构造证明； (2) 通过用于检查假设违规的运行时监控以及对生成逻辑规范的可执行变体的新颖支持，增强从已验证工件中提取可执行代码的能力；（3）通过检测脆弱的证明脚本以及学习常见的转换来促进大型证明存储库的维护。此外，为了增加对证明工程工具链的信任，研究人员开发了针对证明助手核心组件的测试技术。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。