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
From Distributed SAT to Distributed SMT? Successes and Challenges
The last years have brought substantial advancements to parallel and distributed SAT solving, including distributed clause-sharing solving that scales to thousands of cores, distributed incremental SAT solving, scalable proof production, and flexible multi-tasking of many (incremental) SAT tasks. This talk discusses to which degree SMT solving can profit from this technology. I touch on prior works on parallel and distributed SMT solving, outline our recent work on massively parallel bit-precise verification (combining the sequential bit-blasting SMT solver Bitwuzla with the distributed SAT platform Mallob), and discuss potential future directions for parallelizing general SMT solving.