Symbolic Analysis of Programs

Part of the Lecture Notes in Computer Science book series (LNCS, volume 2628)


Programming tools and compilers require sophisticated techniques to statically reason about program semantics. Existing program analysis techniques often fail to give precise answers about the meaning of a program due to imprecise approximations. In order to overcome the deficiencies of existing program analysis approaches we have continued the research in the field of symbolic analysis [53], [17], [97], [52], [15], [16]. Symbolic analysis is a static, global program analysis that examines each expression of the input program only once and attempts to derive a precise mathematical characterization of the computations. The result of this analysis is called “program context” [53], which comprises program semantics for an arbitrary program point. The program context is a symbolic representation of variable values or behaviors arising at run-time of the program. Therfore, symbolic analysis can be seen as a compiler that translates a program into a different language. As a target language we employ symbolic expressions and symbolic recurrences.


Path Condition Recurrence System Symbolic Expression Symbolic Evaluation Conditional Expression 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Copyright information

© Springer-Verlag Berlin Heidelberg 2003

Personalised recommendations