DROPS

Document

Certifying Algorithms for Automated Reasoning (Dagstuhl Seminar 25231)

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

Published in: Dagstuhl Reports, Volume 15, Issue 6 (2026)

Abstract

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.

Cite as

Nikolaj S. Bjørner, Marijn J. H. Heule, Daniela Kaufmann, Jakob Nordström, and Wietze Koops. Certifying Algorithms for Automated Reasoning (Dagstuhl Seminar 25231). In Dagstuhl Reports, Volume 15, Issue 6, pp. 1-31, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{bjorner_et_al:DagRep.15.6.1,
  author =	{Bj{\o}rner, Nikolaj S. and Heule, Marijn J. H. and Kaufmann, Daniela and Nordstr\"{o}m, Jakob and Koops, Wietze},
  title =	{{Certifying Algorithms for Automated Reasoning (Dagstuhl Seminar 25231)}},
  pages =	{1--31},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2026},
  volume =	{15},
  number =	{6},
  editor =	{Bj{\o}rner, Nikolaj S. and Heule, Marijn J. H. and Kaufmann, Daniela and Nordstr\"{o}m, Jakob and Koops, Wietze},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DagRep.15.6.1},
  URN =		{urn:nbn:de:0030-drops-255798},
  doi =		{10.4230/DagRep.15.6.1},
  annote =	{Keywords: ATP, Computer Algebra, DRAT, DRUP, MIP, Propagation Redundancy, QBF, SAT, SMT}
}

Artifact

Software

DOI: 10.4230/artifacts.23376

TalisMan

Authors: Clemens Hofstadler and Daniela Kaufmann

Abstract

Cite as

Clemens Hofstadler, Daniela Kaufmann. TalisMan (Software, Source Code). Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@misc{dagstuhl-artifact-23376,
   title = {{TalisMan}}, 
   author = {Hofstadler, Clemens and Kaufmann, Daniela},
   note = {Software, version 1.0., swhId: \href{https://archive.softwareheritage.org/swh:1:dir:8af022a61661d2b7fb281abbdc2f18d51f221c20;origin=https://github.com/d-kfmnn/talisman;visit=swh:1:snp:d83634ac4675c6c2a76a146bbea12568e3c642a1;anchor=swh:1:rev:be8187df3d18d3530bd175136d6865269cbc21e2}{\texttt{swh:1:dir:8af022a61661d2b7fb281abbdc2f18d51f221c20}} (visited on 2025-08-08)},
   url = {https://github.com/d-kfmnn/talisman/tree/be8187d},
   doi = {10.4230/artifacts.23376},
}

Document

DOI: 10.4230/LIPIcs.CP.2025.14

Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification

Authors: Clemens Hofstadler and Daniela Kaufmann

Published in: LIPIcs, Volume 340, 31st International Conference on Principles and Practice of Constraint Programming (CP 2025)

Abstract

Formal verification of arithmetic circuits using computer algebra has been shown to be highly successful. The circuit is encoded as a system of polynomials, which automatically generates a lexicographic Gröbner basis. Correctness is then verified by computing the polynomial remainder of the specification. To optimize the remainder computation, prior work extracts linear polynomials. However, this required recomputing a Gröbner basis with respect to a degree-compatible order. In this paper, we show that this computationally expensive step is unnecessary and propose a novel hybrid verification approach that combines an FGLM-style linearization technique with a guess-and-prove method using SAT solving to derive the linear relations directly from lexicographic Gröbner bases. We enhance our approach using caching techniques and propagating vanishing monomials. Our experimental results demonstrate that our method significantly outperforms previous linearization techniques.

Cite as

Clemens Hofstadler and Daniela Kaufmann. Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification. In 31st International Conference on Principles and Practice of Constraint Programming (CP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 340, pp. 14:1-14:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{hofstadler_et_al:LIPIcs.CP.2025.14,
  author =	{Hofstadler, Clemens and Kaufmann, Daniela},
  title =	{{Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification}},
  booktitle =	{31st International Conference on Principles and Practice of Constraint Programming (CP 2025)},
  pages =	{14:1--14:22},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-380-5},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{340},
  editor =	{de la Banda, Maria Garcia},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CP.2025.14},
  URN =		{urn:nbn:de:0030-drops-238752},
  doi =		{10.4230/LIPIcs.CP.2025.14},
  annote =	{Keywords: Computer Algebra, FGLM, And-Inverter Graphs, Hardware Verification}
}

Search Results

Documents authored by Kaufmann, Daniela

Certifying Algorithms for Automated Reasoning (Dagstuhl Seminar 25231)

Abstract

Cite as

TalisMan

Abstract

Cite as

Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification

Abstract

Cite as

Thanks for your feedback!

Could not send message