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 and Jan STREJČEK

Basic information

Original name

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

Authors

AYAZIOVÁ, Paulína (703 Slovakia, belonging to the institution) and Jan STREJČEK (203 Czech Republic, guarantor, belonging to the institution)

Edition

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, p. 341-346, 6 pp. 2024

Publisher

Springer

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Germany

Confidentiality degree

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

Publication form

electronic version available online

References:

URL

Impact factor

Impact factor: 0.402 in 2005

Organization unit

Faculty of Informatics

ISBN

978-3-031-57255-5

ISSN

DOI

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

UT WoS

001284187100018

Keywords in English

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

Abstract

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.

Links

GA23-06506S, research and development project

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

Investor: Czech Science Foundation, Advanced Analysis and Verification for Advanced Software

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

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

Investor: Masaryk University, Modeling, analysis, and verification (2024)

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

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

Investor: Masaryk University

Citovat

AYAZIOVÁ, Paulína and 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, p. 341-346. ISBN 978-3-031-57255-5. Available from: 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 and 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, p.~341-346. ISBN~978-3-031-57255-5. Available from: https://dx.doi.org/10.1007/978-3-031-57256-2\_{}18.

Detailed Information on Publication Record