Temporal Logic-driven Symbolic Execution with the Clang Static Analyzer

Symbolic execution is a way of modelling the program state without executing it. It can be used to reason about the behaviour of the program statically. One of the use cases for using symbolic execution is finding software bugs. Clang Static Analyzer can perform static analysis using symbolic execution, and the specific problems to detect are described in imperative C++ code. One of the alternative ways of describing software bugs is linear temporal logic. This approach leads to a declarative description of the problem and allows for a higher level of abstraction. We present a mapping between the declarative temporal logic approach and the imperative Clang Static Analyzer implementation, highlighting the semantic equivalences of temporal logical formulas and C++ programs explicitly focusing on finding bugs statically. We briefly show the implementation details of our extension and present how to use temporal logic for symbolic execution in a powerful manner.