Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution

Varování

Publikace nespadá pod Pedagogickou fakultu, ale pod Fakultu informatiky. Oficiální stránka publikace je na webu muni.cz.

Autoři	JONÁŠ Martin KUMOR Kristián NOVÁK Jakub SEDLÁČEK Jindřich TRTÍK Marek ZAORAL Lukáš AYAZIOVÁ Paulína STREJČEK Jan
Rok publikování	2024
Druh	Článek ve sborníku
Konference	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
Fakulta / Pracoviště MU	Fakulta informatiky
Citace
www	https://link.springer.com/book/10.1007/978-3-031-57256-2_29
Doi	http://dx.doi.org/10.1007/978-3-031-57256-2_29
Klíčová slova	symbolic execution; software verification; Symbiotic
Popis	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.
Související projekty:	Pokročilá analýza a verifikace pro pokročilý software Zapojení studentů Fakulty informatiky do mezinárodní vědecké komunity 24 Modelování, analýza a verifikace (2024)