Symbolic Analysis via Semantic Reinterpretation

Abstract. 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, mutuallyconsistent 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.

• Type: Conference
• Year: 2009
• Where: SPIN
• Authors: Junghee Lim, Akash Lal, Thomas W. Reps
• Keywords: SPIN 2009, Symbolic Program Analysis, Symbolic-analysis Primitives, Theoretical Computer Science, Weakest Liberal Precondition