The Dagstuhl Seminar aims to advance the state of the art in the integration of proof logging with symbolic solvers, and to establish deeper contacts between different research communities working on certifying algorithms where interaction has previously been quite limited or non-existent. The intention is to achieve this broad goal by assembling stakeholders in the SAT, CP, MIP, SMT, ATP, and other closely related communities, including leading researchers in the areas of solver development, deployment of solver tools in applications, and design of proof logging techniques. Concretely, the seminar should:

1. Connect automated-reasoning experts from the different domains around proof-logging techniques.
2. Infuse the communities with new insights into the practical integration of proof logging and methods to develop formally verified proof checkers.
3. Facilitate technology transfer between different research areas in automated reasoning; in particular, concerning techniques for certifying correctness.

A backdrop for the seminar is the wide adoption of automated reasoning within the past decades for developing formally verified software and in the context of combinatorial optimization. The foundation is built on automated deduction algorithms that are used for determining the satisfiability of propositional logic (SAT), first-order logic (ATP), and arithmetic formulas (MIP), constraint programming (CP) and satisfiability modulo theories (SMT). Certification of automated reasoning systems, whether for verification or optimization, is vital to form a trusted base for correctness of safety-critical systems such as control systems for trains and airplanes and to ensure guaranteed optimal answers where the cost of low-quality answers can carry a high monetary or societal impact.

Algorithms used in symbolic solvers are often stunningly powerful in practice and are today used routinely to solve large-scale real-world problems in a wide range of application areas. But the “dirty little secret” is that they are sometimes wrong. It is well documented that even the best CP and MIP solvers sometimes return “solutions” that do not satisfy the constraints, or erroneously claim optimality, and that verification tools can erroneously claim a set of constraints is infeasible when, on the contrary, it has a solution. Also, in more complex scenarios, where solvers are used to solve subproblems, even seemingly innocuous off-by-one mistakes can snowball into huge overall errors.

The goal of the seminar is to contribute to a fundamental shift in how the computer science community thinks about algorithms, so that in the future algorithms will be expected to not just produce an output but to prove that this output is in fact correct.

Creative Commons BY 4.0

Nikolaj S. Bjørner, Marijn J. H. Heule, Daniela Kaufmann, and Jakob Nordström