Symbolic Analysis via Semantic Reinterpretation

Junghee Lim, Akash Lal, and Thomas Reps
University of Wisconsin

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)