[Proof Complexity] 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

​