Witch 3: Validation of Violation Witnesses in the Witness
Format 2.0

D 2024

Witch 3: Validation of Violation Witnesses in the Witness Format 2.0

AYAZIOVÁ, Paulína a Jan STREJČEK

Základní údaje

Originální název

Witch 3: Validation of Violation Witnesses in the Witness Format 2.0

Autoři

AYAZIOVÁ, Paulína (703 Slovensko, domácí) a Jan STREJČEK (203 Česká republika, garant, domácí)

Vydání

Cham (Švýcarsko), Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III, od s. 341-346, 6 s. 2024

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-57255-5

ISSN

DOI

http://dx.doi.org/10.1007/978-3-031-57256-2_18

UT WoS

001284187100018

Klíčová slova anglicky

Witch;witness-validator;SV-COMP;verification witness

Štítky

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

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 18. 10. 2024 16:59, prof. RNDr. Jan Strejček, Ph.D.

Anotace

V originále

Witch 3 is a new validator of violation witnesses in the witness format 2.0. Note that our previous tool, Symbiotic-Witch 2, can validate only violation witnesses in the old GraphML format. Witch 3 validates witnesses of reachability of an error function, overflows, and invalid dereferences and deallocations. Similarly to Symbiotic-Witch 2, the tool is based on symbolic execution and uses parts of the Symbiotic framework. Support of the witness format 2.0 in Witch 3 includes features not supported by Symbiotic-Witch 2, such as constraints on the program variables and function return values, specifying statements by column, and providing the concrete statement in which the violation occurs. These additional features can further restrict the explored state space, and, more importantly, allow for much more precise validation.

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/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 a Jan STREJČEK. Witch 3: Validation of Violation Witnesses in the Witness Format 2.0. Online. In Bernd Finkbeiner and Laura Kovács. Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III. Cham (Švýcarsko): Springer, 2024, s. 341-346. ISBN 978-3-031-57255-5. Dostupné z: https://dx.doi.org/10.1007/978-3-031-57256-2_18.

@inproceedings{2396437,
   author = {Ayaziová, Paulína and Strejček, Jan},
   address = {Cham (Švýcarsko)},
   booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III},
   doi = {http://dx.doi.org/10.1007/978-3-031-57256-2_18},
   editor = {Bernd Finkbeiner and Laura Kovács},
   keywords = {Witch;witness-validator;SV-COMP;verification witness},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham (Švýcarsko)},
   isbn = {978-3-031-57255-5},
   pages = {341-346},
   publisher = {Springer},
   title = {Witch 3: Validation of Violation Witnesses in the Witness Format 2.0},
   url = {https://link.springer.com/book/10.1007/978-3-031-57256-2_18},
   year = {2024}
}

TY  - JOUR
ID  - 2396437
AU  - Ayaziová, Paulína - Strejček, Jan
PY  - 2024
TI  - Witch 3: Validation of Violation Witnesses in the Witness Format 2.0
PB  - Springer
CY  - Cham (Švýcarsko)
SN  - 9783031572555
KW  - Witch;witness-validator;SV-COMP;verification witness
UR  - https://link.springer.com/book/10.1007/978-3-031-57256-2_18
N2  - Witch 3 is a new validator of violation witnesses in the witness format 2.0. Note that our previous tool, Symbiotic-Witch 2, can validate only violation witnesses in the old GraphML format. Witch 3 validates witnesses of reachability of an error function, overflows, and invalid dereferences and deallocations. Similarly to Symbiotic-Witch 2, the tool is based on symbolic execution and uses parts of the Symbiotic framework. Support of the witness format 2.0 in Witch 3 includes features not supported by Symbiotic-Witch 2, such as constraints on the program variables and function return values, specifying statements by column, and providing the concrete statement in which the violation occurs. These additional features can further restrict the explored state space, and, more importantly, allow for much more precise validation.
ER  -

AYAZIOVÁ, Paulína a Jan STREJČEK. Witch 3: Validation of Violation Witnesses in the Witness Format 2.0. Online. In Bernd Finkbeiner and Laura Kovács. \textit{Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III}. Cham (Švýcarsko): Springer, 2024, s.~341-346. ISBN~978-3-031-57255-5. Dostupné z: https://dx.doi.org/10.1007/978-3-031-57256-2\_{}18.

Podrobný výpis o publikaci