Další formáty:
BibTeX
LaTeX
RIS
@inproceedings{2396437, author = {Ayaziová, Paulína and Strejček, Jan}, address = {Cham (Švýcarsko)}, booktitle = {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}, doi = {http://dx.doi.org/10.1007/978-3-031-57256-2_18}, editor = {Bernd Finkbeiner and Laura Kovács}, keywords = {Witch;witness-validator;SV-COMP;verification witness}, howpublished = {elektronická verze "online"}, language = {eng}, location = {Cham (Švýcarsko)}, isbn = {978-3-031-57255-5}, pages = {341-346}, publisher = {Springer}, title = {Witch 3: Validation of Violation Witnesses in the Witness Format 2.0}, url = {https://link.springer.com/book/10.1007/978-3-031-57256-2_18}, year = {2024} }
TY - JOUR ID - 2396437 AU - Ayaziová, Paulína - Strejček, Jan PY - 2024 TI - Witch 3: Validation of Violation Witnesses in the Witness Format 2.0 PB - Springer CY - Cham (Švýcarsko) SN - 9783031572555 KW - Witch;witness-validator;SV-COMP;verification witness UR - https://link.springer.com/book/10.1007/978-3-031-57256-2_18 N2 - 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. ER -
AYAZIOVÁ, Paulína a Jan STREJČEK. Witch 3: Validation of Violation Witnesses in the Witness Format 2.0. Online. In Bernd Finkbeiner and Laura Kovács. \textit{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}. Cham (Švýcarsko): Springer, 2024, s.~341-346. ISBN~978-3-031-57255-5. Dostupné z: https://dx.doi.org/10.1007/978-3-031-57256-2\_{}18.
|