Program visualization refers to the use of graphics to illustrate some aspect of a program execution. Proper visual representations can significantly enhance the understanding of complex computations. The objective of this project is to formulate and evaluate a new methodology for the visualization of concurrent computations, which is to derive visualizations from a program's assertional-type proofs rather than from a program's structure or operations. Based on the reasoning about program states by a proof system, the visualization will be specified in a declarative style as a mapping from program states to a three-dimensional world which is rendered by some graphics display device. A prototype visualization testbed to be built will ultimately consist of a 64-node NCUBE-7 multicomputer connected via a fiber optic link to a Silicon Graphics IRIS-4D graphics workstation.
