<div class="csl-bib-body">
<div class="csl-entry">Hofstadler, C., & Kaufmann, D. (2025). Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification. In M. Garcia de la Banda (Ed.), <i>31st International Conference on Principles and Practice of Constraint Programming (CP 2025)</i>. Schloss Dagstuhl. https://doi.org/10.4230/LIPIcs.CP.2025.14</div>
</div>
-
dc.identifier.uri
http://hdl.handle.net/20.500.12708/222930
-
dc.description.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.
en
dc.description.sponsorship
FWF - Österr. Wissenschaftsfonds
-
dc.language.iso
en
-
dc.relation.ispartofseries
Leibniz International Proceedings in Informatics (LIPIcs)
-
dc.subject
And-Inverter Graphs
en
dc.subject
Computer Algebra
en
dc.subject
FGLM
en
dc.subject
Hardware Verification
en
dc.title
Guess and Prove: A Hybrid Approach to Linear Polynomial Recovery in Circuit Verification
en
dc.type
Inproceedings
en
dc.type
Konferenzbeitrag
de
dc.contributor.affiliation
Johannes Kepler University of Linz, Austria
-
dc.contributor.editoraffiliation
Monash University, Australia
-
dc.relation.isbn
978-3-95977-380-5
-
dc.relation.issn
1868-8969
-
dc.relation.grantno
ESP 666-N
-
dc.type.category
Full-Paper Contribution
-
tuw.booktitle
31st International Conference on Principles and Practice of Constraint Programming (CP 2025)
-
tuw.container.volume
340
-
tuw.peerreviewed
true
-
tuw.relation.publisher
Schloss Dagstuhl
-
tuw.relation.publisherplace
Leibniz
-
tuw.project.title
Wortbasiertes Reasoning mit Computeralgebra und SAT
-
tuw.researchTopic.id
I1
-
tuw.researchTopic.name
Logic and Computation
-
tuw.researchTopic.value
100
-
tuw.publication.orgunit
E192-04 - Forschungsbereich Formal Methods in Systems Engineering
-
tuw.publisher.doi
10.4230/LIPIcs.CP.2025.14
-
dc.description.numberOfPages
22
-
tuw.author.orcid
0000-0002-3025-0604
-
tuw.editor.orcid
0000-0002-6666-514X
-
tuw.event.name
31st International Conference on Principles and Practice of Constraint Programming (CP 2025)
en
tuw.event.startdate
10-08-2025
-
tuw.event.enddate
15-08-2025
-
tuw.event.online
On Site
-
tuw.event.type
Event for scientific audience
-
tuw.event.place
Glasgow
-
tuw.event.country
GB
-
tuw.event.presenter
Hofstadler, Clemens
-
wb.sciencebranch
Informatik
-
wb.sciencebranch
Mathematik
-
wb.sciencebranch.oefos
1020
-
wb.sciencebranch.oefos
1010
-
wb.sciencebranch.value
80
-
wb.sciencebranch.value
20
-
item.openairetype
conference paper
-
item.openairecristype
http://purl.org/coar/resource_type/c_5794
-
item.cerifentitytype
Publications
-
item.languageiso639-1
en
-
item.grantfulltext
none
-
item.fulltext
no Fulltext
-
crisitem.author.dept
Johannes Kepler University of Linz, Austria
-
crisitem.author.dept
E192-04 - Forschungsbereich Formal Methods in Systems Engineering