Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution
| Authors | |
|---|---|
| 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 | |
| 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: |