Symbolic Analysis via Semantic Reinterpretation
Junghee Lim, Akash Lal, and Thomas Reps
The paper presents a novel technique to create implementations of the basic
primitives used in symbolic program analysis:
forward symbolic evaluation,
weakest liberal precondition, and
symbolic composition.
We used the technique to create a system in which,
for the cost of writing just one specification -- an interpreter
for the programming language of interest -- one obtains
automatically-generated, mutually-consistent
implementations of all three symbolic-analysis primitives.
This can be carried out even for languages with pointers and
address arithmetic.
Our implementation has been used to generate symbolic-analysis
primitives for the x86 and PowerPC instruction sets.
(Click here to access the paper:
PDF;
(c) Springer-Verlag.)