Symbolic Execution for Advanced Program Reasoning

Abstract

This thesis addresses a number of program reasoning problems faced by programmers, using symbolic execution. Symbolic execution has the advantage of avoiding "infeasible" paths in the program (paths that cannot be exercised for any input), exploring which could provide spurious information about the program, misleading the programmer. However, as symbolic execution considers the feasibility of individual paths, the number of which could be exponential in general, it suffers from path explosion. To tackle this, we use the technique of "interpolation".

We make significant contributions to the areas of program slicing, verification, concolic testing and trace comprehension. Our breakthroughs in program slicing include formulating the most precise slicing algorithm and the novel notion of "tree slicing". We also bring, for the first time, exponential benefits of interpolation to concolic testing, improve the performance of interpolation-based verifiers, and make strides in the understanding of execution traces using interpolants and loop invariant discovery.