Symbolic Execution and Software Testing
Păsăreanu Corina S. · NATO science for peace and security series. D, Information and communication security · 2013
Symbolic execution is a well-known program analysis technique that executes a program on symbolic inputs which represent all possible concrete program inputs. It systematically explores the program behaviors, while computing the values of conditions and variables in the program as constraints and expressions over the symbolic inputs. Solving the symbolic constraints yields test inputs that guarantee high coverage of the program. Symbolic execution has become very popular in recent years, due to both algorithmic advances and availability of computational power and efficient decision procedures. We review different flavors of symbolic execution, ranging from generalized symbolic execution to dynamic symbolic execution or concolic testing.