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 · Lecture notes in computer science · 2024
Abstract Symbiotic 10 brings four substantial improvements. First, we extended our clone ofKleecalledJetKleewithlazy memory initialization. With this extension,JetKleecan symbolically execute a function without knowing its context. In SV-COMP, we use it to handle variables. Second, we have implemented the technique calledcompact symbolic executiontoSlowbeast. Third, we have implemented a non-trivialmay-happen-in-parallelanalysis, which improves slicing of parallel programs. Finally, we have implemented support for violation witnesses in the newwitness format 2.0.