Trace-based Program Analysis
Christopher Colby and Peter Lee


We present trace-based program analysis, a semantics-based
framework for statically analyzing and transforming programs with
loops, assignments, and nested record structures.  Trace-based
analyses are based on transfer transition systems, which define the
small-step operational semantics of programming languages.
Intuitively, transfer transition systems provide direct support for
reasoning about the possible execution trace of a program, instead of
just individual program states.  The traces in a transfer transition
system have many uses, including the finite representation of all
possible terminating executions of a loop.  Also, traces may be
systematically "pieced together", thus allowing the composition of
separately analyzed program fragments.  The utility of the approach is
demonstrated by showing three applications: software pipelining,
loop-invariant removal, and data alias detection.