M.: Symbiotic: synergy of instrumentation, slicing, and symbolic execution

Abstract. Symbiotic is a tool for detection of bugs described by fi-nite state machines in C programs. The tool combines three well-known techniques: instrumentation, program slicing, and symbolic execution. This paper briefly describes the approach of Symbiotic including its strengths, weaknesses, and modifications for SV-COMP 2013. Architec-ture and installation of the tool are described as well. 1 Verification Approach Symbiotic implements our technique [4] that combines instrumentation, pro-gram slicing, and symbolic execution in order to detect bugs described by finite state machines. More precisely, we instrument a given program with code that tracks runs of state machines representing various erroneous behaviors. If an in-strumented state machine enters an error location during a program execution, then the original program contains a bug specified by the machine. After instru-mentation, we slice [5] the program to reduce its size without affecting runs of state machines. Finally, we symbolically execute [3] the sliced program to fin