Software Verification Witnesses 2.0

D 2025

Software Verification Witnesses 2.0

AYAZIOVÁ, Paulína; Dirk BEYER; Marian LINGSCH-ROSENFELD; Martin SPIESSL; Jan STREJČEK et. al.

Základní údaje

Originální název

Software Verification Witnesses 2.0

Autoři

AYAZIOVÁ, Paulína; Dirk BEYER; Marian LINGSCH-ROSENFELD; Martin SPIESSL a Jan STREJČEK

Vydání

Cham (Švýcarsko), Model Checking Software - 30th International Symposium, SPIN 2024, od s. 184-203, 20 s. 2025

Nakladatel

Springer

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Německo

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Odkazy

URL

Impakt faktor

Impact factor: 0.402 v roce 2005

Organizační jednotka

Fakulta informatiky

ISBN

978-3-031-66148-8

ISSN

DOI

https://doi.org/10.1007/978-3-031-66149-5_11

UT WoS

001419456200011

EID Scopus

2-s2.0-85207659931

Klíčová slova anglicky

verification witnesses; software verification; validation; exchange format; invariant; counterexample

Štítky

formal verification, formela-conference, formela-ver, program analysis, verification

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 9. 10. 2025 17:42, prof. RNDr. Jan Strejček, Ph.D.

Anotace

V originále

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.

Návaznosti

GA23-06506S, projekt VaV

Název: Pokročilá analýza a verifikace pro pokročilý software

Investor: Grantová agentura ČR, Pokročilá analýza a verifikace pro pokročilý software

MUNI/A/1592/2023, interní kód MU

Název: Modelování, analýza a verifikace (2024)

Investor: Masarykova univerzita, Modelování, analýza a verifikace (2024)

MUNI/A/1600/2024, interní kód MU

Název: Modelování, analýza a verifikace (2025)

Investor: Masarykova univerzita, Modelování, analýza a verifikace (2025)

MUNI/A/1608/2023, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 24

Investor: Masarykova univerzita, Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 24

Citovat

AYAZIOVÁ, Paulína; Dirk BEYER; Marian LINGSCH-ROSENFELD; Martin SPIESSL a Jan STREJČEK. Software Verification Witnesses 2.0. Online. In Thomas Neele and Anton Wijs. Model Checking Software - 30th International Symposium, SPIN 2024. Cham (Švýcarsko): Springer, 2025, s. 184-203. ISBN 978-3-031-66148-8. Dostupné z: https://doi.org/10.1007/978-3-031-66149-5_11.

@inproceedings{2425639,
   author = {Ayaziová, Paulína and Beyer, Dirk and LingschandRosenfeld, Marian and Spiessl, Martin and Strejček, Jan},
   address = {Cham (Švýcarsko)},
   booktitle = {Model Checking Software - 30th International Symposium, SPIN 2024},
   doi = {https://doi.org/10.1007/978-3-031-66149-5_11},
   editor = {Thomas Neele and Anton Wijs},
   keywords = {verification witnesses; software verification; validation; exchange format; invariant; counterexample},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham (Švýcarsko)},
   isbn = {978-3-031-66148-8},
   pages = {184-203},
   publisher = {Springer},
   title = {Software Verification Witnesses 2.0},
   url = {https://link.springer.com/chapter/10.1007/978-3-031-66149-5_11},
   year = {2025}
}

TY  - CONF
ID  - 2425639
AU  - Ayaziová, Paulína - Beyer, Dirk - Lingsch-Rosenfeld, Marian - Spiessl, Martin - Strejček, Jan
PY  - 2025
TI  - Software Verification Witnesses 2.0
PB  - Springer
CY  - Cham (Švýcarsko)
SN  - 9783031661488
KW  - verification witnesses
KW  - software verification
KW  - validation
KW  - exchange format
KW  - invariant
KW  - counterexample
UR  - https://link.springer.com/chapter/10.1007/978-3-031-66149-5_11
N2  - 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.
ER  -

AYAZIOVÁ, Paulína; Dirk BEYER; Marian LINGSCH-ROSENFELD; Martin SPIESSL a Jan STREJČEK. Software Verification Witnesses 2.0. Online. In Thomas Neele and Anton Wijs. \textit{Model Checking Software - 30th International Symposium, SPIN 2024}. Cham (Švýcarsko): Springer, 2025, s.~184-203. ISBN~978-3-031-66148-8. Dostupné z: https://doi.org/10.1007/978-3-031-66149-5\_{}11.

Přehled o publikaci