Nullstellensatz-Proofs for Multiplier Verification
Sprache des Vortragstitels:
Englisch
Original Tagungtitel:
CASC 2020
Sprache des Tagungstitel:
Englisch
Original Kurzfassung:
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:
Englisch
Vortragstyp:
Hauptvortrag / Eingeladener Vortrag auf einer Tagung
Forschungs-