2026-07-24T08:23:05Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:25579 2026-03-19T13:48:41Z ddc:004 open_access

Certifying Algorithms for Automated Reasoning (Dagstuhl Seminar 25231) Bjørner, Nikolaj S. Heule, Marijn J. H. Kaufmann, Daniela Nordström, Jakob Koops, Wietze ATP Computer Algebra DRAT DRUP MIP Propagation Redundancy QBF SAT SMT 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 reasoning algorithms used are often very complex, and even the best current algorithms at times produce wrong results. As these tools 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 immensely useful, cannot guarantee correctness, and state-of-the-art algorithms are far beyond what techniques for producing formally verified software can handle. The focus of this Dagstuhl Seminar was the approach of addressing such issues by designing certifying algorithms using so-called proof logging, meaning that algorithms output not only a result but also a machine-verifiable proof of correctness. This proof can then be fed to a dedicated proof checker for verification. Crucially, such proofs should require low overhead to generate and be easy to check, but still supply 100% correctness guarantees. Besides ensuring correctness of outputs for complex algorithms, proof logging can also provide new tools for algorithm development and analysis, software debugging, and even research into explainability in the context of AI. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Nikolaj S. Bjørner and Marijn J. H. Heule and Daniela Kaufmann and Jakob Nordström and Wietze Koops 2026 Is Part Of Dagstuhl Reports, Volume 15, Issue 6 (2026) Article Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/DagRep.15.6.1 urn:nbn:de:0030-drops-255798 https://drops.dagstuhl.de/entities/document/10.4230/DagRep.15.6.1 eng https://creativecommons.org/licenses/by/4.0/legalcode