Symbiotic-Witch: A Klee-Based Violation Witness Checker

D 2022

Symbiotic-Witch: A Klee-Based Violation Witness Checker

AYAZIOVÁ, Paulína, Marek CHALUPA and Jan STREJČEK

Basic information

Original name

Symbiotic-Witch: A Klee-Based Violation Witness Checker

Authors

AYAZIOVÁ, Paulína (703 Slovakia, belonging to the institution), Marek CHALUPA (203 Czech Republic, 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 - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II, p. 468-473, 6 pp. 2022

Publisher

Springer, Cham

Other information

Language

English

Type of outcome

Stať ve sborníku

Field of Study

10201 Computer sciences, information science, bioinformatics

Country of publisher

Switzerland

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

RIV identification code

RIV/00216224:14330/22:00125695

Organization unit

Faculty of Informatics

ISBN

978-3-030-99526-3

ISSN

DOI

http://dx.doi.org/10.1007/978-3-030-99527-0_33

UT WoS

000782398900033

Keywords in English

Symbiotic;witness-validator;SV-COMP;verification witness

Abstract

V originále

Symbiotic-Witch is a new tool for checking violation witnesses in the GraphML-based format used at SV-COMP since 2015. Roughly speaking, Symbiotic-Witch symbolically executes a given program with Klee and simultaneously tracks the set of nodes the witness automaton can be in. Moreover, it reads the return values of nondeterministic functions specified in the witness and uses them to prune the symbolic execution. The violation witness is confirmed if the symbolic execution reaches an error and the current set of witness nodes contains a matching violation node. Symbiotic-Witch currently supports violation witnesses of reachability safety, memory safety, memory cleanup, and overflow properties.

Links

GA19-24397S, research and development project

Name: Automaty v rozhodovacích procedurách a verifikaci (Acronym: AUTODEV)

Investor: Czech Science Foundation

MUNI/A/1145/2021, interní kód MU

Name: Rozsáhlé výpočetní systémy: modely, aplikace a verifikace XI. (Acronym: SV-FI MAV XI.)

Investor: Masaryk University

MUNI/A/1230/2021, interní kód MU

Name: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 22 (Acronym: SKOMU)

Investor: Masaryk University

Citovat

AYAZIOVÁ, Paulína, Marek CHALUPA and Jan STREJČEK. Symbiotic-Witch: A Klee-Based Violation Witness Checker. Online. In Dana Fisman and Grigore Rosu. Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II. Cham (Švýcarsko): Springer, Cham, 2022, p. 468-473. ISBN 978-3-030-99526-3. Available from: https://dx.doi.org/10.1007/978-3-030-99527-0_33.

@inproceedings{1848418,
   author = {Ayaziová, Paulína and Chalupa, Marek and Strejček, Jan},
   address = {Cham (Švýcarsko)},
   booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II},
   doi = {http://dx.doi.org/10.1007/978-3-030-99527-0_33},
   editor = {Dana Fisman and Grigore Rosu},
   keywords = {Symbiotic;witness-validator;SV-COMP;verification witness},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham (Švýcarsko)},
   isbn = {978-3-030-99526-3},
   pages = {468-473},
   publisher = {Springer, Cham},
   title = {Symbiotic-Witch: A Klee-Based Violation Witness Checker},
   url = {https://link.springer.com/chapter/10.1007/978-3-030-99527-0_33},
   year = {2022}
}

TY  - JOUR
ID  - 1848418
AU  - Ayaziová, Paulína - Chalupa, Marek - Strejček, Jan
PY  - 2022
TI  - Symbiotic-Witch: A Klee-Based Violation Witness Checker
PB  - Springer, Cham
CY  - Cham (Švýcarsko)
SN  - 9783030995263
KW  - Symbiotic;witness-validator;SV-COMP;verification witness
UR  - https://link.springer.com/chapter/10.1007/978-3-030-99527-0_33
N2  - Symbiotic-Witch is a new tool for checking violation witnesses in the GraphML-based format used at SV-COMP since 2015. Roughly speaking, Symbiotic-Witch symbolically executes a given program with Klee and simultaneously tracks the set of nodes the witness automaton can be in. Moreover, it reads the return values of nondeterministic functions specified in the witness and uses them to prune the symbolic execution. The violation witness is confirmed if the symbolic execution reaches an error and the current set of witness nodes contains a matching violation node. Symbiotic-Witch currently supports violation witnesses of reachability safety, memory safety, memory cleanup, and overflow properties.
ER  -

AYAZIOVÁ, Paulína, Marek CHALUPA and Jan STREJČEK. Symbiotic-Witch: A Klee-Based Violation Witness Checker. Online. In Dana Fisman and Grigore Rosu. \textit{Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II}. Cham (Švýcarsko): Springer, Cham, 2022, p.~468-473. ISBN~978-3-030-99526-3. Available from: https://dx.doi.org/10.1007/978-3-030-99527-0\_{}33.

Detailed Information on Publication Record