Compositional Symbolic Execution: Incremental Solving Revisited

Abstract

Symbolic execution can automatically explore different execution paths in a system under test and generate tests to precisely cover them. It has two main advantages - being automatic and thorough within a theory - and has many successful applications. The bottleneck of symbolic execution currently is the computation consumption for complex systems. Compositional Symbolic Execution (CSE) introduces a summarisation module to eliminate the redundancy in the exploration of repeatedly encountered code. In our previous work, we generalised the summarisation for any code fragments instead of functions. In this paper, we transplant this idea onto LLVM with many additional features, one of them being..