When verifiers report an alarm, they export a violation witness (exchangeable counterexample) that helps validate the reachability of that alarm. Conventional wisdom says that this violation witness should be very precise: the ideal witness describes a single error path for the validator to check. But we claim that verifiers overshoot and produce large witnesses with information that makes validation unnecessarily difficult. To check our hypothesis, we reduce violation witnesses to that information that automated fault-localization approaches deem relevant for triggering the reported alarm in the program. We perform a large experimental evaluation on the witnesses produced in the International Competition on Software Verification (SV-COMP 2023). It shows that our reduction shrinks the witnesses considerably and enables the confirmation of verification results that were not confirmable before.


    Access

    Download


    Export, share and cite



    Title :

    Fault Localization on Verification Witnesses


    Additional title:

    Lect.Notes Computer


    Contributors:

    Conference:

    International Symposium on Model Checking Software ; 2024 ; Luxembourg City, Luxembourg April 10, 2024 - April 11, 2024


    Published in:

    Model Checking Software ; Chapter : 12 ; 205-224


    Publication date :

    2024-10-13


    Size :

    20 pages





    Type of media :

    Article/Chapter (Book)


    Type of material :

    Electronic Resource


    Language :

    English




    Software Verification Witnesses 2.0

    Ayaziová, Paulína / Beyer, Dirk / Lingsch-Rosenfeld, Marian et al. | Springer Verlag | 2024

    Free access

    Witnesses

    Rolfe, J. M. / Bekerian, D. A. / International Society of Air Safety Investigators | British Library Conference Proceedings | 1994


    Finding witnesses using fewer random bits

    Shoup, Victor | TIBKAT | 1987