Fuzzing and Delta Debugging And-Inverter Graph Verification Tools
Sprache des Vortragstitels:
16th International Conference on Tests and Proofs ? TAP 2022
Sprache des Tagungstitel:
Ensuring correctness of verification tools is equally important as the correctness of the actual problems they try to establish. In this paper 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 verification 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.