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.)
University of Wisconsin