AYAZIOVÁ, Paulína, Marek CHALUPA a Jan STREJČEK. Symbiotic-Witch: A Klee-Based Violation Witness Checker. Online. In Dana Fisman and Grigore Rosu. 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. Cham (Švýcarsko): Springer, Cham, 2022, s. 468-473. ISBN 978-3-030-99526-3. Dostupné z: https://dx.doi.org/10.1007/978-3-030-99527-0_33. |
Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{1848418, author = {Ayaziová, Paulína and Chalupa, Marek and Strejček, Jan}, address = {Cham (Švýcarsko)}, booktitle = {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}, doi = {http://dx.doi.org/10.1007/978-3-030-99527-0_33}, editor = {Dana Fisman and Grigore Rosu}, keywords = {Symbiotic;witness-validator;SV-COMP;verification witness}, howpublished = {elektronická verze "online"}, language = {eng}, location = {Cham (Švýcarsko)}, isbn = {978-3-030-99526-3}, pages = {468-473}, publisher = {Springer, Cham}, title = {Symbiotic-Witch: A Klee-Based Violation Witness Checker}, url = {https://link.springer.com/chapter/10.1007/978-3-030-99527-0_33}, year = {2022} }
TY - JOUR ID - 1848418 AU - Ayaziová, Paulína - Chalupa, Marek - Strejček, Jan PY - 2022 TI - Symbiotic-Witch: A Klee-Based Violation Witness Checker PB - Springer, Cham CY - Cham (Švýcarsko) SN - 9783030995263 KW - Symbiotic;witness-validator;SV-COMP;verification witness UR - https://link.springer.com/chapter/10.1007/978-3-030-99527-0_33 N2 - 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. ER -
AYAZIOVÁ, Paulína, Marek CHALUPA a Jan STREJČEK. Symbiotic-Witch: A Klee-Based Violation Witness Checker. Online. In Dana Fisman and Grigore Rosu. \textit{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}. Cham (Švýcarsko): Springer, Cham, 2022, s.~468-473. ISBN~978-3-030-99526-3. Dostupné z: https://dx.doi.org/10.1007/978-3-030-99527-0\_{}33.
|