Generating Proof Certificates for a Language-Agnostic Deductive Program Verifier

Explore a 20-minute conference talk from OOPSLA 2023 that presents a method for generating proof certificates in language-agnostic program verification. Learn how researchers propose certifying the correctness of successful verification runs by producing proof certificates that can be checked by a small proof checker. Discover the application of this method to program verification in imperative, functional, and assembly languages, demonstrating its language-agnostic nature. Gain insights into the vision of a language-agnostic program verifier that takes a program, its formal specification, and the formal semantics of the programming language as inputs. Understand how this approach builds upon previous work in rewriting and reachability logic to advance the field of program verification.