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

随着数字化在全球范围内继续扩大，安全关键软件和安全关键软件的开发激增。这方面的例子包括自动驾驶汽车和数字医疗服务和设备。这个项目的新颖性是开发验证方法，以推断工业编程语言中新引入的语言功能，这些功能目前不受最先进的自动验证工具的支持。该项目的影响标志着演绎验证从学术研究过渡到实际应用的关键一步。该项目的成果将提高软件质量、安全性和安全性，为社会带来实实在在的好处。该项目的主要教育影响是研究生和本科生的课程开发(演绎课程审核员将作为一种工具)；对学生的指导；以及对代表性不足群体的推广。项目期间开发的工具将开放源代码。该项目将开发依赖一阶断言和辅助逻辑变量的验证方法，并根据可满足性模理论(SMT)求解器进行推理。这项工作将展示如何通过混合使用程序语句和规范来推理函数值和常见编程模式，这使得规范综合能够减少用户注释开销，同时减少开发人员深入理解底层形式化方法的复杂技术的必要性。因此，这项研究构成了自动演绎程序验证器的理论基础，也是项目中进行原型实施的基础。这一奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.