Symbiotic 10: Lazy Memory Initialization and Compact Symbolic Execution
Martin Jonáš, Kristián Kumor, Jakub Novák, Jindřich Sedláček, Marek Trtík, Lukáš Zaoral, Paulína Ayaziová, Jan Strejček
Abstract
Abstract 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 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 .
Topics & Concepts
Computer scienceInitializationParallel computingProgramming languageTheoretical computer scienceAdvanced Malware Detection TechniquesSoftware Testing and Debugging TechniquesParallel Computing and Optimization Techniques