CRII: SHF: Theoretical Foundations of Verifying Function Values and Reducing Annotation Overhead in Automatic Deductive Verification

CRII：SHF：自动演绎验证中验证函数值和减少注释开销的理论基础

• 批准号: 2348334
• 负责人: Yuyan Bao
• 金额: $ 17.5万
• 依托单位: AUGUSTA UNIVERSITY RESEARCH INSTITUTE, INC.
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2024
• 资助国家: 美国
• 起止时间: 2024-05-01 至 2026-04-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2348334&HistoricalAwards=false
• 关键词: CRII; SHF; Theoretical; Foundations; Verifying

As digitalization continues to expand globally, there is a surge in the development of safety-critical and security-critical software. Examples of this include self-driving cars and digital medical services and devices. This project's novelties are developing verification methodologies to reason about newly introduced language features in industrial programming languages, which are currently unsupported by state-of-the-art automatic verification tools. The project's impacts are marking a pivotal step in transitioning deductive verification from academic research into practical application. The outcome of this project will enhance software quality, safety, and security, offering substantial benefits to society. The project’s primary educational impact is curriculum development at the graduate and undergraduate levels (where the deductive program verifier will be used as a tool); mentoring of students; and outreach to underrepresented groups. The tools developed during the project will be released open source.The project will develop verification methodologies that rely on first-order assertions and auxiliary logical variables, and that are tailored to reasoning by Satisfiability Modulo Theories (SMT) solvers. This work will show how to reason about function values and common programming patterns with a mix of program statements and specifications, which enables specification syntheses that reduces user annotation overhead, while alleviating the necessity for developers to deeply comprehend the intricate techniques of underlying formal methods. Thus, the research forms the theoretical basis of automated deductive program verifiers, as well as a basis for a prototype implementation undertaken in the project.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.

随着数字化在全球范围内的不断扩展，关键和关键安全软件的开发也会激增。其中的示例包括自动驾驶汽车，数字医疗服务和设备。该项目的新颖性正在开发验证方法，以推理工业编程语言中新引入的语言功能，这些语言目前不受最新的自动验证工具的支持。该项目的影响标志着将演绎验证从学术研究转换为实际应用的关键步骤。该项目的结果将增强软件质量，安全性和安全性，从而为社会带来可观的好处。该项目的主要教育影响是研究生和本科级别的课程开发（在此使用演绎计划验证者作为工具）；学生的指导；并与代表性不足的群体进行宣传。该项目将在项目期间开发的工具开源。项目将开发依赖一阶断言和辅助逻辑变量的验证方法，这些变量是根据可满足性模型理论（SMT）求解器量身定制的。这项工作将展示如何与程序语句和规格的混合在一起来推理功能值和通用编程模式，从而使规范合成以减少用户注释开销的规范，同时减轻开发人员必要的必要条件，以深入理解基本正式方法的复杂技术。这是该研究的理论基础的自动演绎计划验证者的理论基础，也构成了项目中实施原型实施的基础。该奖项反映了NSF的法定使命，并被认为是通过基金会的知识分子优点和更广泛的影响审查标准通过评估来获得的支持。