DROPS

Artifact

Software

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 Hofstadler, Clemens

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