Interleaving Symbolic Execution and Partial Evaluation

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 partial evaluation comes from symbolic execution itself which makes it natural to interleave partial evaluation and symbolic execution steps in a software verification setup.

• Type: Journal
• Year: 2009
• Where: FMCO
• Authors: Richard Bubel, Reiner Hähnle, Ran Ji
• Keywords: FMCO 2009, Formal Methods, Partial Evaluation, Symbolic Execution, Symbolic Execution Steps