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

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216224%3A14330%2F24%3A00135863" target="_blank" >RIV/00216224:14330/24:00135863 - isvavai.cz</a>

Výsledek na webu

<a href="https://link.springer.com/book/10.1007/978-3-031-57256-2_18" target="_blank" >https://link.springer.com/book/10.1007/978-3-031-57256-2_18</a>

DOI - Digital Object Identifier

<a href="http://dx.doi.org/10.1007/978-3-031-57256-2_18" target="_blank" >10.1007/978-3-031-57256-2_18</a>

Jazyk výsledku

angličtina

Název v původním jazyce

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

Popis výsledku v původním jazyce

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.

Název v anglickém jazyce

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

Popis výsledku anglicky

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.

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)

Projekt

<a href="/cs/project/GA23-06506S" target="_blank" >GA23-06506S: Pokročilá analýza a verifikace pro pokročilý software</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

Rok uplatnění

2024

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ů

Název statě ve sborníku

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

ISBN

9783031572555

ISSN

0302-9743

e-ISSN

1611-3349

Počet stran výsledku

6

Strana od-do

341-346

Název nakladatele

Springer

Místo vydání

Cham (Švýcarsko)

Místo konání akce

Luxembourg City, Luxembourg

Datum konání akce

1. 1. 2024

Typ akce podle státní příslušnosti

WRD - Celosvětová akce

Kód UT WoS článku

001284187100018