MIAO video seminar: Verified proof checkers
Title: Verified proof checkers
Speaker: Magnus Myreen, Chalmers University of Technology
Host: Jacob Nordström, Department of Computer Science, Lund University Joint with
Where: Online - link by registration
Solvers, such as e.g. SAT solvers, are often complicated pieces of software. How can we trust their results? For highly optimised state-of-the-art solvers, testing is insufficient and proving the functional correctness of the solver's implementation is not practically possible. Fortunately, solvers can often be augmented to produce proof certificates that can be checked by separate simpler proof checkers. In recent years, there has been growing interest in formally proving that the proof checkers will never accept a certificate that contains flaws.
In this talk, I will describe work that makes it possible to prove functional correctness of proof checkers down to the machine code that runs them. I have worked on (and have supervised work on) several checkers. In this talk, I'll focus on (1) my work on proving end-to-end correctness of Jared Davis's Milawa prover, and (2) recent work on a LPR/LRAT checker for UNSAT proofs. My talk will include a description of the CakeML project, which was the context of (2). I will use demos to show what the tools look like when running.
Please register at lth.se/digitalth/events/register in order to get an access link to the zoom platform.
The MIAO video seminars are arranged by the Mathematical Insights into Algorithms for Optimization (MIAO) research group at the University of Copenhagen and Lund University. Most of our seminars consist of two parts: first a 50-55-minute regular talk, and then after a break an optional ca-1-hour in-depth technical presentation with (hopefully) a lot of interaction. The intention is that the first part of the seminar will give all listeners a self-contained overview of some exciting research results. For listeners who are particularly interested, there is then an opportunity to return for a second part where we get into more technical details.