[Proof Complexity] PhD defence by Andy Oertel Fri May 29 at 13:30 CEST

[Jakob Nordström]

Dear all,

It is an immense pleasure to announce that on*Friday May 29 at 13:30CEST* Andy Oertel will defend his PhD thesis titled/"Certifying Combinatorial Optimization: A Unified Approach Using Pseudo-Boolean Reasoning"./

The PhD defence will take place in room E:1406 in the E building on Klas Anshelms väg 10 / Ole Römers väg 3 at Lund University, but it is also possible to follow on Zoom usinghttps://lu-se.zoom.us/j/62120595427?pwd=WxX7P4o79C4XRQAfrwmQPaunS1ieBh.1.

The full thesis is available athttps://portal.research.lu.se/en/publications/certifying-combinatorial-optimization-a-unified-approach-using-ps/.

More information about the defence and an abstract can be found below.

Best regards
Jakob Nordström

------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------

*Thesis title*: Certifying Combinatorial Optimization: A Unified Approach Using Pseudo-Boolean Reasoning
*Author*: Andy Oertel, Department of Computer Science, Lund University
*Faculty opponent*: Professor Emeritus Randal E. Bryant, Carnegie Mellon University, USA

*Examination Committee*:

  * Professor Erika Ábrahám, RWTH Aachen, Germany
  * Associate Professor Justin Pearson, Uppsala University
  * Associate Professor Monika Seisenberger, Swansea University, The United Kingdom
  * Deputy: Associate Professor Paul Stankovski Wagner, Lund University

*Session chair*: Professor Görel Hedin, Lund University

*Supervisors*:

  * Main supervisor: Professor Jakob Nordström
  * Associate Senior Lecturer Susanna F. de Rezende

*Abstract*:

Combinatorial optimization is a powerful way to solve complex problems, like planning, scheduling, or hardware verification, by expressing the problem in a mathematical form using discrete variables that can be solved by general solvers. Due to major advances in algorithms for solving combinatorial optimization problems, these solvers can tackle real-world challenges efficiently. However, as solvers become more powerful, they also become larger and more complex, which makes it harder to trust that their output is correct. Ensuring that the solver gives a correct answer becomes especially important when mistakes could have serious consequences, e.g., when solvers are used to match organ donors and recipients or dispatch ambulances.

Testing the solver, which verifies correctness only on known input-output pairs, provides no guarantee that the solver returns correct answers on untested inputs, and therefore we can not fully trust that the answer is correct. Formal verification can prove that a solver adheres to a formal specification and thus guarantees that the answer of the solver is correct, but this approach remains infeasible for modern solvers. The approach that has proven most effective for providing correctness guarantees for solver outputs is certifying algorithms. The idea behind certifying algorithms is that the algorithm generates a certificate that shows the correctness of the result. An independent tool can then use the certificate to verify that the result is correct with respect to the input. This verification tool can be simple enough to enable formal verification of its correctness, ensuring that its verdict can be trusted.

This thesis presents the first viable certification approach for several combinatorial optimization solvers that had previously been considered out of reach. This is achieved through a multipurpose certification system built on so-called pseudo-Boolean reasoning, which enables the generation of correctness certificates across a wide range of different solver paradigms. Developing a multipurpose system allows the checker to be reused for all types of solvers, which sets our work apart from previous, more specialized approaches. Although we use pseudo-Boolean reasoning to certify the solver output, the solver itself does not need to perform pseudo-Boolean reasoning, and making a solver certifying does not require any changes to its internal reasoning. We have also developed a checker that is formally verified to be correct to ensure that this checker can be trusted.


Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +45 28 78 38 11 / +46 70 742 21 98
https://jakobnordstrom.se