A Practical Polynomial Calculus for Arithmetic Circuit Verification

Authors: Daniela Ritirc, Armin Biere and Manuel Kauers

Paper Information

Title:A Practical Polynomial Calculus for Arithmetic Circuit Verification
Authors:Daniela Ritirc, Armin Biere and Manuel Kauers
Proceedings:SCSC Papers
Editors: Anna Maria Bigatti and Martin Brain
Keywords:Multiplier Verification, Computer Algebra, Gröbner Basis, Automatic Proof checking, Polynomial Calculus

ABSTRACT. Generating and automatically checking proofs independently increases confidence in the results of automated reasoning tools. The use of computer algebra is an essential ingredient in recent substantial improvements to scale verification of arithmetic gate-level circuits, such as multipliers, to large bit-widths. There is also a large body of work on theoretical aspects of propositional algebraic proof systems in the proof complexity community starting with the seminal paper introducing the polynomial calculus. We show that the polynomial calculus provides a frame-work to define a practical algebraic calculus (PAC) proof format to capture low-level algebraic proofs needed in scalable gate-level verification of arithmetic circuits. We apply these techniques to generate proofs obtained as by-product of verifying gate-level multipliers using state-of-the-art techniques. Our experiments show that these proofs can be checked efficiently with independent tools.

Talk:Jul 11 16:30 (Session 67F: Research papers)