Informace o publikaci
Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution
| Autoři | |
|---|---|
| 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 | |
| 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: |