To be held on 19th July 2026 in Lisbon, Portugal as part of the Federated Logic Conference (FLoC '26).
Abstract submissions now open.
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 discuss 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.
The purpose of the third edition of WHOOPS is to bring together researchers interested in certification for combinatorial algorithms and automated reasoning. We solicit contributed talks that will be of interest to this audience, on topics which could include:
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.
Deadline: 15th May 2026.
WHOOPS will be held on 19th July 2026 in Lisbon, Portugal as part of the Federated Logic Conference (FLoC '26) workshop program. All speakers and attendees are expected to register for FLoC.