Summarizations for Symbolic Executions
Joxan Jaffar, Andrew Santosa and Razvan Voicu
Abstract
Consideration of execution paths is basic in program analysis and
verification because it represents the process of exact propagation
through the program fragment at hand. This is challenged by the fact
that there are exponentially many paths in general. In this paper, we
consider a straight-line program fragment annotated with initial and
final assertions, and present an optimization technique for this
problem based on the use of {\it summarizations}: partial descriptions
of the input-output behavior of a program fragment. The main
advantage of a summarization is that, during program reasoning,
invocations of the program fragment using different contexts may be
handled by the one summarization.
The key idea is a method for deriving summarizations dynamically.
Traditionally, summarizations are sought for predefined procedures.
In contrast, we compute, opportunistically and on-the-fly,
summarizations of arbitrary program fragments. The objective is to to
discover its most general form, and to discover its most specific
conclusion. This enhances the likelihood that the summarization is
both frequently applicable and effective in future.