Methods are discussed that enhance program analysis. One aspect of the invention
includes a method for checking a model of a program. The method includes a control-flow
graph having vertices from the model, applying a transfer function to each vertex
to form a set of path edges, and analyzing the set of path edges of a vertex. The
set of path edges includes valuations that are implicitly represented so as to
inhibit an undesired explosion in the valuations that would hinder the act of analyzing.
