Call for contributions: 3rd International Workshop on Highlights in Organizing and Optimizing Proof-logging Systems (WHOOPS '26)

[Jakob Nordström]

Dear colleagues,

We would be most grateful for your assistance in distributing the information that 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), immediately before the CP and SAT conferences.

The purpose of WHOOPS is to bring together researchers interested in certifying algorithms and proof logging for automated reasoning and combinatorial solving. As such, we solicit contributed talks that will be of interest to such an 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 presentations 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 instalment 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
- Jakob Nordström, University of Copenhagen and Lund University
- Michael Rawson, University of Southampton
- Adrian Rebola-Pardo, TU Wien

Here is hoping to see you in Lisbon this summer!

Best regards,
Jakob Nordström

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