Abstract
--------
Symbolic trajectory evaluation is a model checking approach based on
partial order representation of state spaces. It computes the
next-state function using symbolic simulation. Symbolic trajectory
evaluation has been successful in dealing with large circuits which
prompts an examination of the approach to determine if it is
applicable for verifying software.

This research report presents a suitable logical framework for model
checking software: the program logic (PLF) and its associated
satisfaction relation, based on the quaternary logic Q. PLF is
appropriate for expressing the truth of propositions about partially
ordered state spaces. Using this framework verification conditions
called assertions are defined and verified.

Symbolic trajectory evaluation still suffers from the state explosion
problem.  Compositionality is an approach that has been successfully
combined with symbolic trajectory evaluation to overcome this
problem. A primary contribution of this research report is the
development of a compositional theory for PLF assertions.

To show the practical use of the symbolic trajectory evaluation and
its compositional theory, a verification system is constructed
integrating theorem proving and symbolic trajectory evaluation:
theorem proving is used as a deductive framework; symbolic trajectory
evaluation as a decision procedure. Data is manipulated efficiently by
symbolic data representation methods.

Experiments are undertaken using this system. These experiments show
that symbolic trajectory evaluation is feasible, and through the use
of its associated compositional theory it is possible to verify some
interesting problems completely.