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://dx.doi.org/10.1007/978-3-031-30820-8_30.
Další formáty:   BibTeX LaTeX RIS
Základní údaje
Originální název Symbiotic-Witch 2: More Efficient Algorithm and Witness Refutation
Autoři AYAZIOVÁ, Paulína (703 Slovensko, 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 - 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
Originální 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"
WWW 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 0302-9743
Doi http://dx.doi.org/10.1007/978-3-031-30820-8_30
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ěnil Změnil: RNDr. Pavel Šmerk, Ph.D., učo 3880. Změněno: 7. 4. 2024 23:35.
Anotace
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 VaVNá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 MUNá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
VytisknoutZobrazeno: 28. 5. 2024 06:37