Information Technology Reference
In-Depth Information
Interleaving Symbolic Execution and
Partial Evaluation
Richard Bubel, Reiner Hahnle, and Ran Ji
Department of Computer Science and Engineering
Chalmers University, 41296 Gothenburg, Sweden
{
bubel,reiner,ran.ji
}
@chalmers.se
Abstract.
Partial evaluation is a program specialization technique that
allows to optimize programs for which partial input is known. We show
that partial evaluation can be used with advantage to speed up as well
symbolic execution of programs. Interestingly, the input required for par-
tial evaluation comes from symbolic execution itself which makes it nat-
ural to interleave partial evaluation and symbolic execution steps in a
software verification setup.
1
Introduction
Symbolic execution [1] and partial evaluation [2] both are generalizations of stan-
dard interpretation of programs, however, they generalize in different ways: while
symbolic execution permits interpretation of a program with symbolic (i.e., un-
specified) initial values, the aim of partial evaluation is to transform a program
with partially specified input values into a (hopefully, more ecient) program
that has only the unspecified arguments as input. For fully specified input argu-
ments the result of both mechanisms is standard program interpretation.
In this paper we show that both technologies not only are compatible with
each other, but that there is considerable potential for synergies. Specifically, we
integrate a simple partial evaluator for a
-like language into the logic-based
symbolic execution engine of the software verification tool KeY [3]. This allows
to interleave symbolic execution and partial evaluation steps within a uniform
(logic-based) framework in a sound way. Intermittent partial evaluation during
symbolic execution has the effect that the remaining program that is yet to be
executed is continuously simplified relative to the current path conditions and
the current symbolic state in each symbolic execution trace.
This paper is organized as follows: in the next section we introduce a small
object-oriented programming language which is used for the formal definitions
(the actual system is implemented for nearly full-fledged sequential
Java
); we
also provide background on symbolic execution and partial evaluation. Sect. 3
defines the program logic and deduction system that we use as a framework for
Java
This work has been partially supported by the EU project FP7-ICT-2007-3 HATS
Highly Adaptable and Trustworthy Software using Formal Methods
and the EU
COST Action IC0701
Formal Verification of Object-Oriented Software
.
