European Research Network on Formal Proofs
COST action CA20111
COST logo
EU flag and COST acknowledgement
COST (European Cooperation in Science and Technology) is a funding agency for research and innovation networks. Our Actions help connect research initiatives across Europe and enable scientists to grow their ideas by sharing them with their peers. This boosts their research, career and innovation.

Date: 13-14 September 2025

Venue: Institut Pascal, 530 Rue André Rivière, 91400 Orsay [access] [hotels] [food options]

Registration/funding requests: fill in this form (registration is free but mandatory)

Background and Purpose

Since the turn of the millennium there have been dramatic improvements in algorithms for combinatorial solving and optimization. The flipside of this is that as the methods get increasingly sophisticated, it becomes increasingly harder to avoid bugs sneaking in during algorithm design and implementation, and it is well documented that even the most mature tools currently available sometimes return incorrect results. 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 combinatorial solvers. During the last ten years the Boolean satisfiability (SAT) solving community has instead successfully introduced 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 algorithmic paradigms such as SAT-based optimization (MaxSAT), constraint programming, and mixed integer linear programming have met with very limited success. This has changed in the last few years with the introduction of pseudo-Boolean (PB) proof logging. Pseudo-Boolean proofs operate with 0-1 integer linear inequalities using a version of the cutting planes proof system, but have turned out to be a very convenient format also for algorithms that reason in terms of very different concepts. The VeriPB tool developed by the Mathematical Insights into Algorithms for Optimization (MIAO) research group in Copenhagen/Lund and its collaborators has so far been shown to support efficient proof logging not only for advanced SAT solving techniques previously beyond reach (including symmetry breaking), but also for MaxSAT solving, subgraph solving, constraint programming, and presolving techniques in 0-1 integer linear programming.

Last year, the (somewhat spontaneous) idea arose to gather researchers from all over Europe working on pseudo-Boolean proof logging in Copenhagen. Reflecting the rather improvised nature of this event, it has been named the 1st Workshop on Highlights in Organizing and Optimizing Proof-logging Systems, or WHOOPS for short. Given last year’s success, the second iteration of this meeting is now planned (as part of the EuroProofNet symposium).

Schedule and programme:

To be announced