Daniela Kaufmann, Armin Biere,
"Fuzzing and Delta Debugging And-Inverter Graph Verification Tools"
: International Conference on Tests and Proofs (TAP), 2022, Serie Lecture Notes in Computer Science (LNCS), Vol. volume 13361, Seite(n) 69-88, 6-2022
Original Titel:
Fuzzing and Delta Debugging And-Inverter Graph Verification Tools
Sprache des Titels:
Englisch
Original Buchtitel:
International Conference on Tests and Proofs (TAP), 2022
Original Kurzfassung:
Ensuring correctness of verification tools is equally important
as the correctness of the actual problems they try to establish. In this pa-
per we evaluate automated fuzzing and debugging techniques applied to
state-of-the-art multiplier verification tools, which take the common gate-
level representation of and-inverter graphs as input. With a generation-
and mutation-based fuzzing approach our tools are able to uncover major
faults in verification tools including crashes as well as inaccurate verifica-
tion results. Additionally we demonstrate the usefulness of certificates for
automated reasoning tools. We further apply delta debugging techniques
and show their effectiveness in reducing failure-inducing inputs.
Forschungs-