An Investigation Into a Probabilistic Framework for Studying Symbolic Execution Based Program Conditioning
Mohammed Daoudi · 2006
This thesis is concerned with program conditioning, a technique which combines symbolic execution [76, 33, 109] and theorem proving [] to identify and remove a set of statements which cannot be executed when a condition of interest holds at some point in a program. It has been applied to problems in maintenance, testing, reuse and reengineering. All current program conditioning algorithms tend to be exponential. This is due to the fact that the computational cost of a conditioning algorithm is dominated by both the exponential growth of the conditioned state and the response time of the theorem prover. This thesis reports on a lightweight approach to program conditioning using the FermaT simplify decision procedure. This is used as a component to ConSUS, a program conditioning system for a subset of the Wide Spectrum Language WSL. The thesis describes the symbolic execution algorithm used by ConSUS, which prunes as it conditions. The thesis also gives analytical evidence that, although exponential in the worst case, on average, the conditioning system reduces its exponential behaviour by several orders of magnitude, thereby making it more effecient than previous approaches.