Daniela Kaufmann, Armin Biere,
"Nullstellensatz-Proofs for Multiplier Verification"
, in François BoulierMatthew EnglandTimur M. SadykovEvgenii V. Vorozhtsov: Proc. Computer Algebra in Scientific Computing (CASC'20), Serie Lecture Notes in Computer Science (LNCS), Vol. 12291, Springer, Seite(n) 368-389, 9-2020
Original Titel:
Nullstellensatz-Proofs for Multiplier Verification
Sprache des Titels:
Englisch
Original Buchtitel:
Proc. Computer Algebra in Scientific Computing (CASC'20)
Original Kurzfassung:
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.
Forschungs-