Symbiotic-Witch: A Klee-Based Violation Witness Checker
Identifikátory výsledku
Kód výsledku v IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F22%3A00125695" target="_blank" >RIV/00216224:14330/22:00125695 - isvavai.cz</a>
Výsledek na webu
<a href="https://link.springer.com/chapter/10.1007/978-3-030-99527-0_33" target="_blank" >https://link.springer.com/chapter/10.1007/978-3-030-99527-0_33</a>
DOI - Digital Object Identifier
<a href="http://dx.doi.org/10.1007/978-3-030-99527-0_33" target="_blank" >10.1007/978-3-030-99527-0_33</a>
Alternativní jazyky
Jazyk výsledku
angličtina
Název v původním jazyce
Symbiotic-Witch: A Klee-Based Violation Witness Checker
Popis výsledku v původním jazyce
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ázev v anglickém jazyce
Symbiotic-Witch: A Klee-Based Violation Witness Checker
Popis výsledku anglicky
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.
Klasifikace
Druh
D - Stať ve sborníku
CEP obor
—
OECD FORD obor
10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)
Návaznosti výsledku
Projekt
<a href="/cs/project/GA19-24397S" target="_blank" >GA19-24397S: Automaty v rozhodovacích procedurách a verifikaci</a><br>
Návaznosti
P - Projekt vyzkumu a vyvoje financovany z verejnych zdroju (s odkazem do CEP)<br>S - Specificky vyzkum na vysokych skolach<br>I - Institucionalni podpora na dlouhodoby koncepcni rozvoj vyzkumne organizace
Ostatní
Rok uplatnění
2022
Kód důvěrnosti údajů
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Údaje specifické pro druh výsledku
Název statě ve sborníku
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
ISBN
9783030995263
ISSN
0302-9743
e-ISSN
—
Počet stran výsledku
6
Strana od-do
468-473
Název nakladatele
Springer, Cham
Místo vydání
Cham (Švýcarsko)
Místo konání akce
Munich, Germany
Datum konání akce
1. 1. 2022
Typ akce podle státní příslušnosti
WRD - Celosvětová akce
Kód UT WoS článku
000782398900033