Symbolic evaluation as a basis for integrated validation

Abstract

Symbolic evaluation derives information about the static and dynamic semantics of programs by means of a static and global program analysis. This information is then deposited in a program data base to be used by various tools supporting program development and validation The theoretical foundations of Symbolic Evaluation were developed at Harvard University. The Harvard Program Development System (PDS) included as a component for semantic analysis a prototype implementation of a symbolic evaluator. This paper presents the model underlying symbolic evaluation and discusses its impact on tools for program development and validation.