| JONÁŠ, Martin, Kristián KUMOR, Jakub NOVÁK, Jindřich SEDLÁČEK, Marek TRTÍK, Lukáš ZAORAL, Paulína AYAZIOVÁ and Jan STREJČEK. Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution. Online. In Bernd Finkbeiner and Laura Kovács. 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, p. 406-411. ISBN 978-3-031-57255-5. Available from: https://dx.doi.org/10.1007/978-3-031-57256-2_29. |
Other formats:
BibTeX
LaTeX
RIS
@inproceedings{2396645,
author = {Jonáš, Martin and Kumor, Kristián and Novák, Jakub and Sedláček, Jindřich and Trtík, Marek and Zaoral, Lukáš and 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_29},
editor = {Bernd Finkbeiner and Laura Kovács},
keywords = {symbolic execution; software verification; Symbiotic},
howpublished = {elektronická verze "online"},
language = {eng},
location = {Cham (Švýcarsko)},
isbn = {978-3-031-57255-5},
pages = {406-411},
publisher = {Springer},
title = {Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution},
url = {https://link.springer.com/book/10.1007/978-3-031-57256-2_29},
year = {2024}
}
TY - JOUR
ID - 2396645
AU - Jonáš, Martin - Kumor, Kristián - Novák, Jakub - Sedláček, Jindřich - Trtík, Marek - Zaoral, Lukáš - Ayaziová, Paulína - Strejček, Jan
PY - 2024
TI - Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution
PB - Springer
CY - Cham (Švýcarsko)
SN - 9783031572555
KW - symbolic execution
KW - software verification
KW - Symbiotic
UR - https://link.springer.com/book/10.1007/978-3-031-57256-2_29
N2 - Symbiotic 10 brings four substantial improvements. First, we extended our clone of Klee called JetKlee with lazy memory initialization. With this extension, JetKlee can symbolically execute a function without knowing its context. In SV-COMP, we use it to handle extern variables. Second, we have implemented the technique called compact symbolic execution to Slowbeast. Third, we have implemented a non-trivial may-happen-in-parallel analysis, which improves slicing of parallel programs. Finally, we have implemented support for violation witnesses in the new witness format 2.0.
ER -
JONÁŠ, Martin, Kristián KUMOR, Jakub NOVÁK, Jindřich SEDLÁČEK, Marek TRTÍK, Lukáš ZAORAL, Paulína AYAZIOVÁ and Jan STREJČEK. Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution. 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, p.~406-411. ISBN~978-3-031-57255-5. Available from: https://dx.doi.org/10.1007/978-3-031-57256-2\_{}29.
|
