Analysis of Loop Programs Using Generalization

This thesis describes a symbolic execution system, PAN, that is able to symbolically execute loops. PAN achieves this by generalizing the effect of a few loop iterations to predict the effect of an unknown number of iterations. PAN operates on relatively unstructured loops that include 'go to' type constructs, allowing multiple exits from a loop. PAN uses a two stage generalization approach using techniques developed in Artificial Intelligence systems. The first stage uses models of expected loop effects and requires only limited search to generalize the effect of simple loops The second stage uses a less constrained approach that can generalize the effects of more complex loops by using extensive search. Fundamental to PAN's generalization method is the sequence. These are identified using models and used in both stages of the generalization process.