Invited Talk
Taming the Polynomial Explosion
A New Approach to Algebraic Circuit Verification
Tuesday, Dec. 3, 2024, 17:00 - 18:00,
Technische Fakultät SR 00-34 Geb. 51
Dr. Daniela Kaufmann
Automated Program Reasoning Group
Faculty of Informatics
TU Wien, Austria
Abstract
Formal verification using computer algebra has emerged as a powerful approach for circuit verification. This technique encodes a circuit, represented as an and-inverter graph, into a set of polynomials that generates a Gröbner basis. Verification relies on computing the polynomial remainder of the specification. But there is a catch: a monomial blow-up often occurs during specification rewriting — a problem that often necessitates dedicated heuristics to manage the complexity.
In this talk, I’ll start with an accessible introduction to Gröbner bases and how they are used in circuit verification. Then, I’ll discuss our novel approach, which shifts the computational effort to rewriting the Gröbner basis itself rather than the specification. By restructuring the basis to include linear polynomials, we tame the monomial blow-up and simplify the rewriting process. Our approach offers promising potential for efficient and scalable formal verification of complex circuits, as our experimental evaluation demonstrates.
Bio
Daniela Kaufmann is a researcher specializing in formal methods, focusing on applying computer algebra to automated reasoning. She currently holds an FWF ESPRIT fellowship at TU Wien in the Automated Program Reasoning (APRe) group. With a PhD in computer science from Johannes Kepler University Linz, her research includes pioneering work in computer algebra and SAT-based methods for verifying arithmetic circuits. Her contributions have earned her notable awards, including the GI-Dissertation Award and the Heinz Zemanek Award.