Symcretic testing of programs

Targeted inputs are input values for a program that lead to the execution of a user-specified branch or statement. Targeted inputs are useful: In debugging, for example, they allow programmers to follow the execution towards the program point where a bug occurred. In testing, they constitute a test case that covers a new piece of code. A natural approach to find targeted inputs is symbolic backward execution. However, symbolic backward execution struggles with complicated arithmetic, external method calls, and data-dependent loops that occur in many real-world programs. This dissertation describes symcretic execution, a novel method for efficiently finding targeted inputs. Symcretic execution overcomes the limitations of symbolic backward execution by integrating it with concrete forward execution. The approach consists of two phases: In its first phase, symcretic execution uses symbolic backward execution to find a feasible execution path from the given target to any of the program's entry points. Unlike prior approaches, symcretic execution skips over constraints that are problematic for the symbolic decision procedure and defers their solution until the second phase. The second phase of symcretic execution begins when the symbolic execution reaches an entry point. In this phase, symcretic execution uses concrete forward execution and heuristic search to find inputs that satisfy the constraints that were skipped in the first phase. A comparison with related approaches and an empirical evaluation suggest that symcretic execution finds more inputs that result in relevant executions while avoiding the exploration of uninteresting paths. The heuristic search algorithm employed in the second phase of symcretic execution must be able to handle complicated arithmetic and external method calls. The dissertation therefore introduces an algorithm called concolic walk. The concolic walk algorithm also applies to solving path conditions in customary symbolic and concolic execution and is thus presented in this more general setting. The concolic walk algorithm is a heuristic search based on a geometric interpretation of the task of finding inputs. An evaluation of the algorithm shows that it finds more solutions (and hence improves coverage) than the simplification-based heuristics that have been used in concolic testing. Moreover, the concolic walk algorithm improves the effectiveness of state-of-the-art concolic test generators that are using powerful specialized constraint solvers