Call for contributions: 2nd International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS '25)
Jakob Nordström
Dear colleagues,
This message is a call for contributions to the 2nd International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS '25) on September 13-14, 2025, in Paris.
Please send a message to Jakob Nordström at j...@di.ku.dk if you wish to contribute a presentation on proof logging, certifying algorithms, or verifiably correct results in general for algorithms or problems in combinatorial solving or automated reasoning broadly construed. Presentation slots will be 30 minutes, including time for questions, discussions, and switching speakers. The intention is that contributed talks will be scheduled on Sunday September 14, with Saturday September 13 reserved for longer tutorial-style talks.
For more information about the workshop, please see the text
below or visit the webpage https://jakobnordstrom.se/WHOOPS25/.
We would be most grateful for your assistance in sharing this
information with any colleagues for whom this might be of
interest.
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 in coordination with the EuroProofNet Workshop on Automated
Reasoning and Proof Logging, which is in turn part of
the Final
EuroProofNet Symposium.
More information about the workshop can be found at https://jakobnordstrom.se/WHOOPS25/. Please contact Jakob Nordström if you wish to contribute a presentation.
Background and Purpose
Since the turn of the millennium there have been dramatic improvements in algorithms for combinatorial solving and optimization. The flipside of this is that as the methods get increasingly sophisticated, it becomes increasingly harder to avoid bugs sneaking in during algorithm design and implementation, and even the most mature tools currently available struggle with incorrect results. Software testing, while important, has not been sufficient to resolve this problem, and formal verification methods are far from being able to scale to the level of complexity in modern combinatorial solvers. During the last twenty years the Boolean satisfiability (SAT) solving community has instead spearheaded the use of proof logging, meaning that the SAT solvers have to output, along the answer to a problem, a machine-verifiable proof that this answer is correct. Such solvers are also referred to as certifying algorithms.
For a long time, attempts to extend proof logging to stronger paradigms in combinatorial solving and optimization have 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 a version of the cutting planes proof system, but have turned out to be a very convenient format also for algorithms that reason in terms of very different concepts. The VeriPB tool developed by the Mathematical Insights into Algorithms for Optimization (MIAO) research group in Copenhagen/Lund and its collaborators has so far been shown to support efficient proof logging for paradigms such as SAT-based optimization (MaxSAT), pseudo-Boolean optimization, subgraph solving, constraint programming, automated planning, and presolving in 0-1 integer linear programming, as well as for techniques such as symmetry breaking and dynamic programming.
These developments have been so fast that in 2024 the fairly spontaneous idea arose to gather researchers working on pseudo-Boolean proof logging to an informal gathering, 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 Orsay outside Paris under the auspices of EuroProofNet. While we still expect a healthy dose of pseudo-Boolean proof logging, we are very much hoping to also discuss certifying algorithms for automated reasoning more broadly, including satisfiability modulo theories (SMT) solving and first- and higher-order theorem proving.
Registration
Registration is free but mandatory, and is done by filling in the registration form.
Workshop Program
More information about the program will be available closer to the workshop at https://jakobnordstrom.se/WHOOPS25/. The tentative plans are that:
- Saturday will consist of slightly longer, tutorial-style, talks, explaining how pseudo-Boolean proof logging can support efficient certified solving for paradigms such as SAT-based optimization (MaxSAT), pseudo-Boolean optimization, subgraph solving, constraint programming, automated planning, as well as for techniques such as symmetry breaking and dynamic programming.
- On Sunday we will have contributed talks, where we might still have some presentations of the very latest news in pseudo-Boolean proof logging, but where we are very much hoping to also discuss certifying algorithms for automated reasoning more broadly, including satisfiability modulo theories (SMT) solving and first- and higher-order theorem proving.
Jakob Nordström, Professor
University of Copenhagen and Lund University
Phone: +45 28 78 38 11 / +46 70 742 21 98
https://jakobnordstrom.se