Verification witnesses are now widely accepted objects used not only to confirm or refute verification results, but also for general exchange of information among various tools for program verification. The original format for witnesses is based on GraphML, and it has some known issues including a semantics based on control-flow automata, limited tool support of some format features, and a large size of witness files. This paper presents version 2.0 of the witness format, which is based on YAML and overcomes the above-mentioned issues. We describe the new format, provide an experimental comparison of various aspects of the original and the new witness format showing that both witness formats perform similarly, and report on its adoption in the community.


    Zugriff

    Download


    Exportieren, teilen und zitieren



    Titel :

    Software Verification Witnesses 2.0


    Weitere Titelangaben:

    Lect.Notes Computer


    Beteiligte:
    Neele, Thomas (Herausgeber:in) / Wijs, Anton (Herausgeber:in) / Ayaziová, Paulína (Autor:in) / Beyer, Dirk (Autor:in) / Lingsch-Rosenfeld, Marian (Autor:in) / Spiessl, Martin (Autor:in) / Strejček, Jan (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 : 11 ; 184-203


    Erscheinungsdatum :

    13.10.2024


    Format / Umfang :

    20 pages





    Medientyp :

    Aufsatz/Kapitel (Buch)


    Format :

    Elektronische Ressource


    Sprache :

    Englisch




    Fault Localization on Verification Witnesses

    Beyer, Dirk / Kettl, Matthias / Lemberger, Thomas | 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