Nullstellensatz-Proofs for Multiplier Verification

Description

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.

Period	14 Sept 2020
Event title	CASC 2020
Event type	Conference
Location	AustriaShow on map