Symbiotic 9: String Analysis and Backward Symbolic Execution with Loop Folding

Marek Chalupa, Vincent Mihalkovič, Anna Řechtáčková, Lukáš Zaoral, Jan Strejček

2022Lecture notes in computer science22 citationsDOI Open Access PDF

Abstract

Abstract The development of Symbiotic 9 focused mainly on two components. One is the symbolic executor Slowbeast , which newly supports backward symbolic execution including its extension called loop folding . This technique can infer inductive invariants from backward symbolic execution states. Thanks to these invariants, Symbiotic 9 is able to produce non-trivial correctness witnesses, which is a feature that is missing in previous versions of Symbiotic . We have also extended forward symbolic execution in Slowbeast with a basic support for parallel programs. The second component with significant improvements is the instrumentation module. In particular, we have extended the static analysis of accesses to arrays with features designed for programs that manipulate C strings. Symbiotic 9 is the Overall winner of SV-COMP 2022. Moreover, it won also the categories MemSafety and SoftwareSystems , and placed third in FalsificationOverall .

Topics & Concepts

Computer scienceExecutorSymbolic executionCorrectnessString (physics)Programming languageFolding (DSP implementation)Loop (graph theory)Extension (predicate logic)Symbolic data analysisTheoretical computer scienceMathematicsLawSoftwarePolitical scienceMathematical physicsElectrical engineeringCombinatoricsEngineeringAdvanced Malware Detection TechniquesSoftware Testing and Debugging TechniquesSoftware Engineering Research