Symbolic Execution for Advanced Program Reasoning

Abstract:

This thesis aims to address a number of program reasoning problems faced every
day by programmers, using the technique of 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 and mislead 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 make use of the technique of "interpolation".

Using this, we make significant contributions to the areas of program slicing,
verification, concolic testing and trace comprehension. Our breakthroughs in the
area of slicing include formulating the most precise slicing algorithm and the
novel notion of "tree slicing". We introduce the concept of "speculation" which,
for the first time, brings the exponential benefits of interpolation to concolic
testing and improves the performance of interpolation-based verifiers. We also
make strides in the understanding and explanation of execution traces using
interpolants and loop invariant discovery.