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@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/
/
**********************************************************
*
* Contributions to be spread via DMANET are submitted to
*
* DMANET@zpr.uni-koeln.de
*
* Replies to a message carried on DMANET should NOT be
* addressed to DMANET but to the original sender. The
* original sender, however, is invited to prepare an
* update of the replies received and to communicate it
* via DMANET.
*
* DISCRETE MATHEMATICS AND ALGORITHMS NETWORK (DMANET)
* http://www.zaik.uni-koeln.de/AFS/publications/dmanet/
*
**********************************************************
Posts
