Symbiotic-Witch: A Klee-Based Violation Witness Checker

Result code in 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>

Result on the web

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

Result language

angličtina

Original language name

Symbiotic-Witch: A Klee-Based Violation Witness Checker

Original language description

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.

Czech name

—

Czech description

—

Type

D - Article in proceedings

CEP classification

—

OECD FORD branch

10201 - Computer sciences, information science, bioinformathics (hardware development to be 2.2, social aspect to be 5.8)

Project

<a href="/en/project/GA19-24397S" target="_blank" >GA19-24397S: Automata for Decision Procedures and Verification</a><br>

Continuities

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

Publication year

2022

Confidentiality

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Article name in the collection

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

—

Number of pages

6

Pages from-to

468-473

Publisher name

Springer, Cham

Place of publication

Cham (Švýcarsko)

Event location

Munich, Germany

Event date

Jan 1, 2022

Type of event by nationality

WRD - Celosvětová akce

UT code for WoS article

000782398900033