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

Executive Summary

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.

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 ten 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 techniques 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 in Europe 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 and Travel Funding

Registration is free but mandatory, and is done by filling in the registration form.

As part of the registration, it is also possible to apply for travel funding from EuroProofNet. Please note that the application deadline for funding requests is already May 25, 2025. See also information about the formal eligibility rules.

Venue

WHOOPS '25 will be held at Institut Pascal at 530 Rue André Rivière, 91400 Orsay (see map).

We will also provide the option of attending the workshop online (barring unexpected technical hiccups).

Please follow the links for information about local travel directions, nearby hotels, and food options.

On Sunday, the institute building will be locked for security reasons, but a number of access cards will be distributed among WHOOPS '25 participants. To be on the safe side, it might be a good idea to write down the cell phone number of the WHOOPS '25 main organizer Jakob Nordström, so that you can call if you would accidentally get locked out. Note also that dining selections on Sunday September 14 are very limited and so some advance planning is highly recommended. The symposium organizers advise to buy some food for lunch at the Supermarket Intermarché Express on Sunday morning.

Workshop Program

More information about the program will be available closer to the workshop.

The tentative plans are as follows:

Saturday will probably mostly 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.

Please contact Jakob Nordström if you would be interested in giving a presentation at the WHOOPS '25 workshop (virtually or on site).

Organizers

The WHOOPS '25 workshop is organized by Jakob Nordström at the University of Copenhagen and Lund University in collaboration with Ciaran McCreesh at the University of Glasgow.