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.


    Zugriff

    Download


    Exportieren, teilen und zitieren



    Titel :

    Fault Localization on Verification Witnesses


    Weitere Titelangaben:

    Lect.Notes Computer


    Beteiligte:
    Neele, Thomas (Herausgeber:in) / Wijs, Anton (Herausgeber:in) / Beyer, Dirk (Autor:in) / Kettl, Matthias (Autor:in) / Lemberger, Thomas (Autor:in)

    Kongress:

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


    Erschienen in:

    Model Checking Software ; Kapitel : 12 ; 205-224


    Erscheinungsdatum :

    13.10.2024


    Format / Umfang :

    20 pages





    Medientyp :

    Aufsatz/Kapitel (Buch)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch




    Software Verification Witnesses 2.0

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

    Freier Zugriff

    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