Symbiotic-Witch: A Klee-Based Violation Witness Checker

D 2022

Symbiotic-Witch: A Klee-Based Violation Witness Checker

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

Základní údaje

Originální název

Symbiotic-Witch: A Klee-Based Violation Witness Checker

Autoři

AYAZIOVÁ, Paulína (703 Slovensko, domácí), Marek CHALUPA (203 Česká republika, 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 - 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, od s. 468-473, 6 s. 2022

Nakladatel

Springer, Cham

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Švýcarsko

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

Kód RIV

RIV/00216224:14330/22:00125695

Organizační jednotka

Fakulta informatiky

ISBN

978-3-030-99526-3

ISSN

DOI

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

UT WoS

000782398900033

Klíčová slova anglicky

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

Štítky

formela-ver, program analysis, Symbiotic, verification

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 28. 3. 2023 10:40, RNDr. Pavel Šmerk, Ph.D.

Anotace

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.

Návaznosti

GA19-24397S, projekt VaV

Název: Automaty v rozhodovacích procedurách a verifikaci (Akronym: AUTODEV)

Investor: Grantová agentura ČR, Automata for Decision Procedures and Verification

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

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

Investor: Masarykova univerzita, Rozsáhlé výpočetní systémy: modely, aplikace a verifikace XI.

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

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

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

Citovat

AYAZIOVÁ, Paulína, Marek CHALUPA a 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, s. 468-473. ISBN 978-3-030-99526-3. Dostupné z: 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 a 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, s.~468-473. ISBN~978-3-030-99526-3. Dostupné z: https://dx.doi.org/10.1007/978-3-030-99527-0\_{}33.

Podrobný výpis o publikaci