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的法定使命，并被认为值得通过使用基金会的智力价值和更广泛的影响审查标准进行评估来支持。