A Survey of Symbolic Execution and Its Tool KLEE
Tao Zhang, Pan Wang, Xi Guo · Procedia Computer Science · 2020
Symbolic execution is a highly practical program analysis technology. With the gradual deepening of its research and the continuous maturity of technology itself, it has been widely used in software testing and other fields. KLEE is a symbolic execution tool built on the LLVM compilation framework that automatically generates test cases for high coverage of complex and environmentally intensive programs. This article comprehensively describes the basic principle, development situation, current issues of symbolic execution, and KLEE’s infrastructure as well as the generation of test cases. To some extent, it highlights the unique advantages of symbolic execution in software testing and analysis.