Computer Science Seminar by William Mansky: Formally Verifying C Programs Down to Assembly, Interactively and Automatically
Speaker: , assistant professor of computer science, University of Illinois Chicago
Title: Formally Verifying C Programs Down to Assembly, Interactively and Automatically
Abstract: How can we know that programs do what we intended them to do? Separation logic is a powerful tool for proving correctness of programs, with adequacy theorems that connect our proofs to the actual behavior of executing code. The Iris framework puts this into practice via a machine-checked foundational implementation of separation logic in the Rocq theorem prover. But most instances of Iris are defined on core models or ad-hoc semantics for the programming language under consideration, so the guarantees bottom out at a mathematical model invented by the tool’s designer. In this talk I will explore what it takes to build an Iris instance for a real imperative programming language, namely C as defined by the CompCert verified compiler. The result is a core logic that can integrate multiple verification tools, both interactive and semi-automatic, to obtain formal correctness guarantees on the behavior of C code down to assembly.
Bio: William Mansky has been an assistant professor of computer science at the University of Illinois Chicago since 2018. His areas of expertise are interactive theorem proving, program verification, and concurrency, and he is one of the maintainers of the Verified Software Toolchain (VST) for formally proving correctness of C programs. As a participant in NSF Expedition “The Science of Deep Specification”, he helped verify an HTTP web server and developed theory for connecting program verification systems to verified operating systems. His more recent work focuses on integrating theoretical concurrency models and logics into verification tools for real programming languages.