The 3rd International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS '26) will be held on 19th July 2026 as part of the Federated Logic Conference (FLoC '26).
The purpose of the third edition of WHOOPS is to bring together researchers interested in certification and proof logging for combinatorial algorithms and automated reasoning. Unlike the first two editions, we hope to have a broader focus than just VeriPB and pseudo-Boolean proof logging. As such, we solicit contributed talks that will be of interest to this wider audience, on topics which could include:
- The theory or practice of proof logging systems;
- Bringing proof logging to existing or new solving tools;
- Descriptions of challenges anticipated or encountered;
- Integrating proof logging into larger verification frameworks;
- Connections between proof logging and explainability;
- Speculation about or requests for future directions for proof
logging and certification
WHOOPS does not have full papers or proceedings, and talks may cover work that is already published or that may be published elsewhere in the future. We ask only for a brief (<1 page) abstract, which can be submitted through the FLoC submissions system before the deadline of 15th May 2026. Further details can be found at:
https://ciaranm.github.io/WHOOPS26/
Background and Purpose:
Modern automated reasoning has transformed large parts of industry and has also found numerous scientific applications. But many reasoning problems are computationally very challenging, or sometimes even undecidable. Because of this, the algorithms used are getting increasingly complex, and even the most mature tools currently available struggle with incorrect results. As these algorithms are increasingly being used autonomously, sometimes even in life-critical applications, it is urgent to ensure that what they compute is valid. 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 algorithms.
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 automated reasoning met with limited success. This has changed in the last few years, however, with proof logging techniques now being developed for a wide range of paradigms such as SAT-based and pseudo-Boolean optimisation, subgraph solving, constraint programming, automated planning, mixed integer linear programming, and even satisfiability modulo theories (SMT) solving and automated theorem proving.
These developments have been so fast that in 2024 the fairly spontaneous idea arose to celebrate the latest advances during an informal workshop, 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). The second edition WHOOPS '25 was held last autumn under the auspices of EuroProofNet.
The third installment of the workshop series, to be held on 19th July 2026 as part of the Federated Logic Conference (FLoC '26), will continue to expand the range of topics beyond SAT and pseudo-Boolean proof logging to provide a forum for discussing certifying algorithms for automated reasoning more broadly. In addition to ensuring correctness of outputs for automated reasoning algorithms, we also hope to examine the use of proof logging to provide new tools for algorithm development and analysis, software debugging, and even research into explainability in the context of AI.
Program Committee:
Katalin Fazekas, TU Wien
Daniela Kaufmann, TU Wien
Ciaran McCreesh, University of Glasgow
Michael Rawson, University of Southampton
Adrian Rebola Pardo, TU Wien
Jakob Nordström, University of Copenhagen and Lund University
Hoping to see some of you in Lisbon,
--
Ciaran McCreesh
**********************************************************
*
* 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
