Proving properties of programs using automatically generated models.

Abstract

This thesis describes a method for automatically generating theories in a first order logic with arithmetic for the purpose of proving properties about the programs. We build the logic and define the syntactic model generation algorithm. The models can be used to prove a substantial class of properties that are true of the programs they are generated from. Here, a model is a set of formulas of the logic that are interpreted as mathematical function definitions. These functions describe the computation steps of the algorithm.