Zoom links for proof logging workshop WHOOPS '25 this weekend September 13-14
Jakob Nordström
Dear colleagues,
Due to strong interest, registration to the EuroProofNet Symposium was closed a couple of weeks ago. However, for those of us interested in hearing the very latest news about certifying algorithms and proof logging, it is still possible to join online for the the 2nd International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS ‘25) this coming weekend September 13-14 using the following Zoom links:
- Saturday morning: https://zoom.us/j/95174623006?pwd=9Zjcf8a9noyRe5JlKSPwGurS7BN7wx.1&jst=2 (ID: 95174623006, password: 518746)
- Saturday afternoon: https://zoom.us/j/99810308547?pwd=PnExx2Ncs8FgvcmLFAuqvoBbOzvfoe.1&jst=2 (ID: 99810308547, password: 904113)
- Sunday morning: https://zoom.us/j/91453234939?pwd=CRxiaQOZjOhjr5r5fDMNfhW7zgdfe0.1&jst=2 (ID: 91453234939, password: 408753)
- Sunday afternoon: https://zoom.us/j/98496734995?pwd=mU2vwsHSgrpdNxCMbXYjlHyXavmiga.1&jst=2 (ID: 98496734995, password: 182837)
More information (including schedule) 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.
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