Call for participation in proof logging workshop WHOOPS ‘25 in Paris September 13-14

[Jakob Nordström]

Dear colleagues,

For those of us who heard all the buzz about certifying algorithms and proof logging at CP, SAT, and SoCS last week and want to know more—and perhaps even more for those of us who unfortunately could not make it to Glasgow—this is just to advertise the 2nd International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS ‘25), which will be held in Paris during the weekend September 13-14. More information can be found at https://jakobnordstrom.se/WHOOPS25/ and/or in the text below.

Best regards,
Jakob Nordström

2nd International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS ‘25)

The 2nd International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS ‘25) will be held on September 13-14, 2025, at Institut Pascal in Orsay on the outskirts of Paris. More information about the workshop can be found at https://jakobnordstrom.se/WHOOPS25/.

Background and Purpose

Since the turn of the millennium there have been dramatic improvements in algorithms for combinatorial solving and optimization. But as the algorithms get more complex, it becomes increasingly harder to avoid bugs, and even the most mature tools currently available struggle with incorrect results.

During the last twenty years the Boolean satisfiability (SAT) solving community has spearheaded the use of proof logging to address this problem, meaning that solvers have to output, along the answer to a problem, a machine-verifiable proof that this answer is correct. For a long time, attempts to extend such certified solving to stronger paradigms in combinatorial optimization met with limited success, but this has changed in the last few years with the introduction of pseudo-Boolean (PB) proof logging. Pseudo-Boolean proofs operate with 0-1 integer linear inequalities using the cutting planes proof system, but have turned out to be a convenient format also for algorithms that reason in terms of very different concepts.

These developments have been so fast that in 2024 the spontaneous idea arose to arrange a get-together for researchers working on proof logging, which—reflecting the rather improvised nature of the event—was named the 1st Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS ‘24). This year, the second edition of the workshop will be held on September 13-14 in Paris under the auspices of EuroProofNet.

Registration

Workshop registration is free but mandatory, and is done by filling in the registration form at https://forms.gle/QLFzh3Ugv5WgkhZr7.

Workshop Program

More detailed information about the workshop program can be found at https://jakobnordstrom.se/WHOOPS25/, but the overall plans are as follows:

• Saturday will consist of slightly longer, tutorial-style, talks, explaining how pseudo-Boolean proof logging can support efficient certified solving for different solving paradigms and techniques.
• On Sunday we will have contributed talks on different proof logging methods and applications as well as on problems for which proof logging remains to be developed.

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

​