Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution

Logo poskytovatele

Varování

Publikace nespadá pod Ekonomicko-správní 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:

Používáte starou verzi internetového prohlížeče. Doporučujeme aktualizovat Váš prohlížeč na nejnovější verzi.