A System to Generate Test Data and Symbolically Execute Programs

TLDR

This paper presents a system that generates test data for ANSI Fortran programs by symbolically executing program paths. The system symbolically executes a given path, formulates constraints on input variables, solves linear constraints with linear programming, detects infeasible paths, augments constraints to simulate errors, and produces symbolic expressions of output variables. The system produces test data that drives execution along specified paths and generates human‑readable symbolic output expressions that aid error detection, assertion generation, and documentation.

Abstract

This paper describes a system that attempts to generate test data for programs written in ANSI Fortran. Given a path, the system symbolically executes the path and creates a set of constraints on the program's input variables. If the set of constraints is linear, linear programming techniques are employed to obtain a solution. A solution to the set of constraints is test data that will drive execution down the given path. If it can be determined that the set of constraints is inconsistent, then the given path is shown to be nonexecutable. To increase the chance of detecting some of the more common programming errors, artificial constraints are temporarily created that simulate error conditions and then an attempt is made to solve each augmented set of constraints. A symbolic representation of the program's output variables in terms of the program's input variables is also created. The symbolic representation is in a human readable form that facilitates error detection as well as being a possible aid in assertion generation and automatic program documentation.