TY - GEN
T1 - Nullstellensatz-Proofs for Multiplier Verification
AU - Kaufmann, Daniela
AU - Biere, Armin
PY - 2020/9
Y1 - 2020/9
N2 - Automated reasoning techniques based on computer algebraare an essential ingredient in formal verification of gate-level multipliercircuits. Generating and independently checking proof certificates helpsto validate the verification results. Two algebraic proof systems, Null-stellensatz and polynomial calculus, are well-known in proof complexity.The practical application of the polynomial calculus has been studiedrecently. However, producing and checking Nullstellensatz certificatesfor multiplier verification has not been considered so far. In this paperwe show how Nullstellensatz proofs can be generated as a by-productof multiplier verification and present our Nullstellensatz proof checkerNuss-Checker. Additionally, we prove quadratic upper bounds on theproof size for simple array multipliers.
AB - Automated reasoning techniques based on computer algebraare an essential ingredient in formal verification of gate-level multipliercircuits. Generating and independently checking proof certificates helpsto validate the verification results. Two algebraic proof systems, Null-stellensatz and polynomial calculus, are well-known in proof complexity.The practical application of the polynomial calculus has been studiedrecently. However, producing and checking Nullstellensatz certificatesfor multiplier verification has not been considered so far. In this paperwe show how Nullstellensatz proofs can be generated as a by-productof multiplier verification and present our Nullstellensatz proof checkerNuss-Checker. Additionally, we prove quadratic upper bounds on theproof size for simple array multipliers.
UR - https://www.scopus.com/pages/publications/85096570767
U2 - 10.1007/978-3-030-60026-6_21
DO - 10.1007/978-3-030-60026-6_21
M3 - Conference proceedings
SN - 9783030600259
VL - 12291
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 368
EP - 389
BT - Proc. Computer Algebra in Scientific Computing (CASC'20)
A2 - Boulier, François
A2 - England, Matthew
A2 - Sadykov, Timur M.
A2 - Vorozhtsov, Evgenii V.
PB - Springer
ER -