[  paper | experiments ]

This page provides access to the source code, benchmarks, and experiments described in our paper at CASC 2020.

Paper

Daniela Kaufmann, Armin Biere.
Nullstellensatz-Proofs for Multiplier Verification.
To appear..
[ paper | bibtex ]

Proof Generation

Our verification tool AMulet is available at GitHub.

Proof Checking

The Nullstellensatz Proof Checker - Nusschecker
[ Nusschecker.tar.xz ] source code (57.9 KB)

Experiments

[ KaufmannBiere-CASC-20-benchmarks.tar.xz ] benchmarks (9.4 MB)
[ KaufmannBiere-CASC-20-data.tar.xz ] data (30.5 MB)