Nullstellensatz-Proofs for Multiplier Verification
Sprache des Vortragstitels:
Sprache des Tagungstitel:
Automated reasoning techniques based on computer algebra are an essential ingredient in formal verification of gate-level multiplier circuits. Generating and independently checking proof certificates helps to validate the verification results. Two algebraic proof systems, Nullstellensatz and polynomial calculus, are well-known in proof complexity. The practical application of the polynomial calculus has been studied recently. However, producing and checking Nullstellensatz certificates for multiplier verification has not been considered so far. In this paper we show how Nullstellensatz proofs can be generated as a by-product of multiplier verification and present our Nullstellensatz proof checker Nusschecker. Additionally, we prove quadratic upper bounds on the proof size for simple array multipliers.
Sprache der Kurzfassung:
Hauptvortrag / Eingeladener Vortrag auf einer Tagung