Symbiotic-Witch 2: More Efficient Algorithm and Witness
Refutation

D 2023

Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation

AYAZIOVÁ, Paulína a Jan STREJČEK

Základní údaje

Originální název

Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation

Autoři

AYAZIOVÁ, Paulína a Jan STREJČEK

Vydání

Cham (Švýcarsko), Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Part II, od s. 523-528, 6 s. 2023

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/23:00131936

Organizační jednotka

Fakulta informatiky

ISBN

978-3-031-30819-2

ISSN

DOI

https://doi.org/10.1007/978-3-031-30820-8_30

UT WoS

001288698100039

EID Scopus

2-s2.0-85161463126

Klíčová slova anglicky

Witch;witness-validator;SV-COMP;verification witness

Štítky

formela-conference, formela-ver, program analysis, Symbiotic, verification

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 13. 8. 2025 17:43, Mgr. Petra Trembecká, Ph.D.

Anotace

V originále

The new version of the witness validator Symbiotic-Witch follows more precisely the (fixed version of the) semantics of verification witnesses. This makes the tool more efficient as it can benefit from sink nodes. Further, the tool can now refute a witness. To sum up, Symbiotic-Witch 2 can confirm or refute violation witnesses of reachability safety, memory safety, memory cleanup, and overflow properties of sequential C programs.

Návaznosti

GA23-06506S, projekt VaV

Název: Pokročilá analýza a verifikace pro pokročilý software

Investor: Grantová agentura ČR, Pokročilá analýza a verifikace pro pokročilý software

MUNI/A/1433/2022, interní kód MU

Název: Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 23

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

Citovat

AYAZIOVÁ, Paulína a Jan STREJČEK. Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation. Online. In Sriram Sankaranarayanan and Natasha Sharygina. Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Part II. Cham (Švýcarsko): Springer, Cham, 2023, s. 523-528. ISBN 978-3-031-30819-2. Dostupné z: https://doi.org/10.1007/978-3-031-30820-8_30.

@inproceedings{2326763,
   author = {Ayaziová, Paulína and Strejček, Jan},
   address = {Cham (Švýcarsko)},
   booktitle = {Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Part II},
   doi = {https://doi.org/10.1007/978-3-031-30820-8_30},
   editor = {Sriram Sankaranarayanan and Natasha Sharygina},
   keywords = {Witch;witness-validator;SV-COMP;verification witness},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Cham (Švýcarsko)},
   isbn = {978-3-031-30819-2},
   pages = {523-528},
   publisher = {Springer, Cham},
   title = {Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation},
   url = {https://link.springer.com/chapter/10.1007/978-3-031-30820-8_30},
   year = {2023}
}

TY  - CONF
ID  - 2326763
AU  - Ayaziová, Paulína - Strejček, Jan
PY  - 2023
TI  - Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation
PB  - Springer, Cham
CY  - Cham (Švýcarsko)
SN  - 9783031308192
KW  - Witch;witness-validator;SV-COMP;verification witness
UR  - https://link.springer.com/chapter/10.1007/978-3-031-30820-8_30
N2  - The new version of the witness validator Symbiotic-Witch follows more precisely the (fixed version of the) semantics of verification witnesses. This makes the tool more efficient as it can benefit from sink nodes. Further, the tool can now refute a witness. To sum up, Symbiotic-Witch 2 can confirm or refute violation witnesses of reachability safety, memory safety, memory cleanup, and overflow properties of sequential C programs.
ER  -

AYAZIOVÁ, Paulína a Jan STREJČEK. Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation. Online. In Sriram Sankaranarayanan and Natasha Sharygina. \textit{Tools and Algorithms for the Construction and Analysis of Systems - 29th International Conference, TACAS 2023, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2023, Paris, France, April 22-27, 2023, Proceedings, Part II}. Cham (Švýcarsko): Springer, Cham, 2023, s.~523-528. ISBN~978-3-031-30819-2. Dostupné z: https://doi.org/10.1007/978-3-031-30820-8\_{}30.

Přehled o publikaci