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

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.