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

[Ciaran McCreesh]

Dear all,

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 CP and SAT.

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 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
Michael Rawson, University of Southampton
Adrian Rebola Pardo, TU Wien
Jakob Nordström, University of Copenhagen and Lund University

See you in Lisbon,
--
Ciaran McCreesh