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 x86 and PowerPC.
(Click here to access the paper:
PDF)
University of Wisconsin