[Proof Complexity] 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 jn at 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 
<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/>/.

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 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 <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 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)/ 
<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

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


    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.

/Please contact Jakob Nordström <https://jakobnordstrom.se/> if you 
would be interested in giving a presentation at the WHOOPS '25 workshop.

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

/