A Heuristic Approach to the Path Explosion Problem for Complex Heap Programs

Abstract

Symbolic verification is a verification method for automatically verifying the correctness of programs, by collecting path constraints which are used to assert specifications and invariants using a third-party constraint solver. In this thesis we have extended OOX, a symbolic verification engine for object oriented programs, with support for subtyping through inheritance and dynamic dispatch, and have implemented a heuristic approach for reducing the path explosion problem. The verification engine operates on programs in the language OOX, which is one of the first intermediate verification languages with support for inheritance.

In the experiments we show that there is an exponential explosion in verification runtime as the number of subtypes of a symbolic object increase in a datastructure. With the aim to improve on this we have implemented an initial heuristic approach to reduce the path explosion problem, by selecting paths with a criterion. We have implemented heuristics based on maximising code coverage, on randomness and a round-robin combination. In our evaluation we found that the performance of the heuristic is dependent on the depth of the input program, with our first results showing that the maximising code coverage heuristic is not feasible for smaller programs.