[Proof Complexity] Seminar Fri Oct 22 at 14:00 CEST with Magnus Myreen: Verified proof checkers

[Jakob Nordström]

Dear all,

On Friday October 22 at 14:00 CEST we are having a MIAO video seminar with Magnus Myreen from Chalmers University of Technology titled "Verified proof checkers". See below for the abstract.

We will meet virtually at https://lu-se.zoom.us/j/61925271827 . Please feel free to share this information with colleagues who you think might be interested. We are also hoping to record the seminar and post on the MIAO Research YouTube channel https://www.youtube.com/channel/UCN0G2Wfl9-sAKrVLVza7z4A for people who would like to hear the talk but cannot attend.

Most of our seminars consist of two parts: first a 50-55-minute regular talk, and then after a break a 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 an overview of some exciting research results, and after the break people who have the time and interest will have the additional opportunity to really get into the technical details. However, for those who feel that the first part was enough, it is perfectly fine to just discretely drop out during the break. No questions asked; no excuses needed.

More information about upcoming video seminars can be found at http://www.jakobnordstrom.se/videoseminars/ . If you do not wish to receive these announcements, or receive several copies of them, please send a message to jakob.nordstrom at cs.lth.se.

Best regards,
Jakob Nordström

**********

Friday Oct 22 at 14:00
Verified proof checkers
(Magnus Myreen, Chalmers University of Technology)

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.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +46 70 742 21 98
http://www.jakobnordstrom.se