[Proof Complexity] MIAO seminar Tue Jun 6 at 14:00 CET with Ciaran McCreesh: Is your combinatorial search algorithm telling the truth?

[Jakob Nordström]

Dear all,

On Tuesday June 6 at 14:00 we will have a seminar with Ciaran McCreesh from the University of Glasgow titled "Is your combinatorial search algorithm telling the truth?" You find the abstract at the bottom of this message.

We will run this as a hybrid seminar at the University of Copenhagen. Local participants are warmly welcome on UCPH campus --- the exact location will be communicated later. Other participants are equally warmly welcome to join 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://youtube.com/@MIAOresearch 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 a self-contained overview of some exciting research results, and after the break people who have the time and interest will get an 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 MIAO seminars can be found at http://www.jakobnordstrom.se/miao-seminars/ . In particular, don't miss the seminar with Malte Helmert on Thursday June 1! If you do not wish to receive these announcements, or receive several copies of them, please send a message to jn at di.ku.dk.

Best regards,
Jakob Nordström

**********

Tuesday Jun 6 at 14:00
Is your combinatorial search algorithm telling the truth?
(Ciaran McCreesh, University of Glasgow)

How do you know whether your combinatorial search algorithm is implemented correctly? You could try testing it, but even if you're convinced you've done a thorough job, will anyone else believe you? Another possibility is "correct by construction" software created using formal methods—but these methods are far from being able to approach the complexity or performance of modern satisfiability or constraint programming solvers. In this talk I'll tell you about a third option, called proof logging or certifying. The idea is that, alongside a solution, an algorithm must produce a mathematical proof in a standard format that demonstrates that the solution is correct. This proof can be verified by an independent proof checker, which should be much simpler, and thus easier to trust. The key challenge in getting this to work is to find a proof language which is both simple to verify, and expressive enough to cover a wide range of solving techniques with very low overheads. It's not obvious that such a language should even exist, but I'll argue that the cutting planes proof system with a dominance-based extension rule might be exactly what we need: even though this proof system has no notion of what vertices, graphs, or even integers are, it is strong enough to verify the reasoning used in state of the art algorithms for problems like subgraph isomorphism, clique, and maximum common connected subgraph, and even in constraint programming solvers.


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