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

[Jakob Nordström]

Dear collleagues,

I would be grateful for your help to advertise that the *2nd 
International Workshop on Highlights in Organizing and Optimizing 
Proof-logging Systems (WHOOPS '25) *will be held on *September 13-14, 
2025, *in Orsay outside Paris. Please note that the*deadline for travel 
funding applications* is already *this Sunday May 25!*

For more information about the workshop, see the text below or the 
webpage https://jakobnordstrom.se/WHOOPS25/. Please feel free to share 
this information with any colleagues who you think might be interested.

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 
<https://www.institut-pascal.universite-paris-saclay.fr/> in Orsay* on 
the outskirts of Paris in coordination with the /EuroProofNet Workshop 
on Automated Reasoning and Proof Logging 
<https://europroofnet.github.io/wg2-symposium/>/, which is in turn part 
of the /Final EuroProofNet Symposium 
<https://europroofnet.github.io/Symposium/>/.

Please note that the *deadline for travel funding applications *is 
already *this Sunday May 25! *More information about the workshop can be 
found at https://jakobnordstrom.se/WHOOPS25/. Please contact Jakob 
Nordström <https://jakobnordstrom.se/> 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 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 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 <https://gitlab.com/MIAOresearch/software/VeriPB>/ tool 
developed by the /Mathematical Insights into Algorithms for Optimization 
(MIAO) <https://jakobnordstrom.se/miao-group/>/ 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)/ 
<https://jakobnordstrom.se/WHOOPS24/>. This year, the second edition of 
the workshop will be held on September 13-14 in Orsay outside Paris 
under the auspices of EuroProofNet <http://europroofnet.github.io/>. 
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 <https://forms.gle/QLFzh3Ugv5WgkhZr7>.

As part of the registration, it is also possible to apply for travel 
funding <https://forms.gle/QLFzh3Ugv5WgkhZr7> from EuroProofNet 
<http://europroofnet.github.io/>. Please note that the *application 
deadline for funding requests* is already *May 25, 2025.* See also 
information about the formal eligibility rules 
<https://europroofnet.github.io/eligibility/>.


    Workshop Program

More information about the program will be available closer to the 
workshop at https://jakobnordstrom.se/WHOOPS25/. 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 <https://jakobnordstrom.se/> if you 
would be interested in giving a presentation at the WHOOPS '25 workshop 
(virtually or on site).

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

/