Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution

Investor logo

Warning

This publication doesn't include Faculty of Economics and Administration. It includes Faculty of Informatics. Official publication website can be found on muni.cz.
Authors

JONÁŠ Martin KUMOR Kristián NOVÁK Jakub SEDLÁČEK Jindřich TRTÍK Marek ZAORAL Lukáš AYAZIOVÁ Paulína STREJČEK Jan

Year of publication 2024
Type Article in Proceedings
Conference 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
MU Faculty or unit

Faculty of Informatics

Citation
Web 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
Keywords symbolic execution; software verification; Symbiotic
Description 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.
Related projects:

You are running an old browser version. We recommend updating your browser to its latest version.