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

To be held on 19th July 2026 in Lisbon, Portugal as part of the Federated Logic Conference (FLoC '26).

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.

Draft Schedule

The schedule below is a draft and is subject to change.

Contributed 1: Proofs (09:00 – 10:30)

• 09:00–09:10 — Opening Remarks
• 09:10–09:30 — Efficient and Reliable Hitting-Set Computations for the Implicit Hitting Set Approach
  Hannes Ihalainen (University of Helsinki), Dieter Vandesande (Vrije Universiteit Brussel & KU Leuven), André Schidler (University of Freiburg), Jeremias Berg (University of Helsinki), Bart Bogaerts (KU Leuven & Vrije Universiteit Brussel), Matti Järvisalo (University of Helsinki)
• 09:30–09:50 — Towards Practical Zero-Knowledge Proof for PSPACE
  Ashwin Karthikeyan (University of Toronto), Hengyu Liu (University of Illinois Urbana-Champaign), Kuldeep S. Meel (University of Toronto, Georgia Institute of Technology), Ning Luo (University of Illinois Urbana-Champaign)
• 09:50–10:10 — Trimming Pseudo-Boolean Proofs
  Berhan Oumer Adame (Vrije Universiteit Brussel, Belgium and Arba Minch University, Ethiopia), Bart Bogaerts (KU Leuven, Belgium and Vrije Universiteit Brussel, Belgium), Benjamin Bogø (University of Copenhagen, Denmark and Lund University, Sweden), Simon Dold (University of Basel, Switzerland), Arthur Gontier (University of Glasgow, United Kingdom), Wietze Koops (Lund University, Sweden and University of Copenhagen, Denmark), Ciaran McCreesh (University of Glasgow, United Kingdom), Matthew J. McIlree (University of Glasgow, United Kingdom), Jakob Nordström (University of Copenhagen, Denmark and Lund University, Sweden), Andy Oertel (Lund University, Sweden and University of Copenhagen, Denmark), Adrian Rebola-Pardo (Vienna University of Technology, Austria and Johannes Kepler University Linz, Austria), Mark Turnbull (University of Glasgow, United Kingdom)
• 10:10–10:30 — Proving back and forth with the same rules
  Peter Pfeiffer (JKU Linz), Adrian Rebola-Pardo (TU Wien, JKU Linz)

Coffee Break (10:30 – 11:00)

Invited Talk: Stefan Szeider (11:00 – 12:00)

From Verdicts to Theorems: Importing LRAT and VeriPB Certificates into Lean 4

Lunch (12:00 – 13:30)

Invited Talk: Haniel Barbosa (13:30 – 14:30)

Proof logging for satisfiability modulo theories solving

Contributed 2: SMT (14:30 – 15:30)

• 14:30–14:50 — Proof Logging for Nonlinear Boundary-Value Solvers: A Falkner-Skan Case Study
  Karthikhesvaran S. S. (Indiana University Bloomington)
• 14:50–15:10 — Certifying Algorithms for Nonlinear Real Arithmetic
  Tomaz Mascarenhas (Universidade Federal de Minas Gerais), Haniel Barbosa (Universidade Federal de Minas Gerais)
• 15:10–15:30 — Pseudo-Boolean Blasting for the SMT Theory of Bit-Vectors
  Pedro Saccomani (Universidade Federal de Minas Gerais), Haniel Barbosa (Universidade Federal de Minas Gerais)

Coffee Break (15:30 – 16:00)

Contributed 3: CP and Encodings (16:00 – 18:00)

• 16:00–16:20 — End-to-End Verification for Constraint Programming: Closing the Encodings Gap
  Wietze Koops (Lund University and University of Copenhagen), Ciaran McCreesh (University of Glasgow), Matthew J. McIlree (University of Glasgow), Magnus O. Myreen (Chalmers University), Jakob Nordström (University of Copenhagen and Lund University), Philip Rodgers (University of Glasgow), Yong Kiam Tan (Nanyang Technological University and Singapore Institute for Infocomm Research), Wei-Lin Wu (Singapore Institute for Infocomm Research)
• 16:20–16:40 — Certificate-Based Propagation: Foundations for Correct Propagator Design
  Maarten Flippo (Delft University of Technology), Imko Marijnissen (Delft University of Technology), Emir Demirović (Delft University of Technology)
• 16:40–17:00 — Generalised Clause Learning for Constraint Programming
  Justin Pearson (Uppsala universitet)
• 17:00–17:20 — How hard can multiplication be?
  Matthew J. McIlree (University of Glasgow), Ciaran McCreesh (University of Glasgow)
• 17:20–17:40 — Proof Logging for (Re)Encoding
  Marijn Heule (Carnegie Mellon University)
• 17:40–18:00 — Discussion and Closing

Venue and Registration

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.

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