Invited Speakers
Daniela Kaufmann, TU Wien, Austria
SAT-Guided Gröbner Basis Methods for Arithmetic Circuit Verification
Formal verification of arithmetic circuits remains a challenging problem at the intersection of SAT solving, SMT, and computer algebra. While SAT-based techniques have achieved remarkable success across many verification domains, arithmetic hardware continues to pose significant challenges. One of the most effective approaches in this setting relies on algebraic reasoning: a circuit, represented as an and-inverter graph, is encoded as a system of polynomials that induces a Gröbner basis, and correctness is established by reducing a polynomial specification with respect to this basis.
In the first part of this talk, I will provide an overview of arithmetic circuit verification and discuss how SAT solving and computer algebra can be combined to discover structural information and enabling simplifications that are difficult to obtain through purely algebraic methods.
In the second part, I will present a recent approach that addresses one of the main bottlenecks of algebraic verification: the monomial blow-up that occurs during specification rewriting. Rather than focusing computational effort on rewriting the specification, we rewrite the Gröbner basis itself to expose useful linear relations using algebraic guesses and SAT-based proofs. The resulting approach significantly simplifies the reduction process and improves the scalability of arithmetic circuit verification.
Dominik Schreiber, Karlsruhe Institute of Technology, Germany
