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 partial evaluation comes from symbolic execution itself which makes it natural to interleave partial evaluation and symbolic execution steps in a software verification setup.
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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
King, J.C.: A program verifier. PhD thesis, Carnegie-Mellon University (1969)
Jones, N.D., Gomard, C.K., Sestoft, P.: Partial evaluation and automatic program generation. Prentice-Hall, Englewood Cliffs (1993)
Beckert, B., Hähnle, R., Schmitt, P. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS, vol. 4334. Springer, Heidelberg (2006)
Beckert, B., Platzer, A.: Dynamic logic with non-rigid functions: A basis for object-oriented program verification. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 266–280. Springer, Heidelberg (2006)
Heisel, M., Reif, W., Stephan, W.: Program verification by symbolic execution and induction. In: Knuth, E., Neuhold, E.J. (eds.) Operating Systems 1982. LNCS, vol. 152, Springer, Heidelberg (1985)
Pasareanu, C.S., Visser, W.: Verification of Java programs using symbolic execution and invariant generation. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 164–181. Springer, Heidelberg (2004)
Barnett, M., Leino, K.R.M., Schulte, W.: The Spec# programming system: an overview. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 49–69. Springer, Heidelberg (2005)
Baum, M.: Debugging by visualizing of symbolic execution. Master’s thesis, Dept.of Computer Science, Institute for Theoretical Computer Science (June 2007)
de Halleux, J., Tillmann, N.: Parameterized unit testing with Pex. In: Beckert, B., Hähnle, R. (eds.) TAP 2008. LNCS, vol. 4966, pp. 171–181. Springer, Heidelberg (2008)
Engel, C., Hähnle, R.: Generating unit tests from formal proofs. In: Gurevich, Y., Meyer, B. (eds.) TAP 2007. LNCS, vol. 4454, pp. 169–188. Springer, Heidelberg (2007)
Stenzel, K.: A formally verified calculus for full Java Card. In: Rattray, C., Maharaj, S., Shankland, C. (eds.) AMAST 2004. LNCS, vol. 3116, pp. 491–505. Springer, Heidelberg (2004)
Deng, X., Lee, J.: Robby: Bogor/Kiasan: a k-bounded symbolic execution for checking strong heap properties of open systems. In: Proc. 21st IEEE/ASM Intl. Conference on Automated Software Engineering, Tokyo, Japan, pp. 157–166. IEEE Computer Society, Los Alamitos (2006)
Jacobs, B., Piessens, F.: The VeriFast program verifier. Technical Report CW-520, Department of Computer Science, Katholieke Universiteit Leuven (August 2008)
Schultz, U.P., Lawall, J.L., Consel, C.: Automatic program specialization for java. ACM Transactions on Programming Languages and Systems 25 (2003)
Bubel, R., Hähnle, R., Weiss, B.: Abstract interpretation of symbolic execution with explicit state updates. In: de Boer, F.S., Bonsangue, M.M., Madelaine, E. (eds.) FMCO 2008. LNCS, vol. 5751, pp. 247–277. Springer, Heidelberg (2009)
Weiß, B.: Predicate abstraction in a program logic calculus. In: Leuschel, M., Wehrheim, H. (eds.) IFM 2009. LNCS, vol. 5423, pp. 136–150. Springer, Heidelberg (2009)
Engel, C., Roth, A., Schmitt, P.H., Weiß, B.: Verification of modifies clauses in dynamic logic with non-rigid functions. Technical Report 2009-9, Department of Computer Science, University of Karlsruhe (2009)
Sahlin, D.: Mixtus: an automatic partial evaluator for full prolog. New Gen. Comput. 12(1), 7–51 (1993)
Glenstrup, A.J., Makholm, H., Secher, J.P.: C-mix: Specialization of c programs. Partial Evaluation, 108–154 (1998)
Turchin, V.F.: The concept of a supercompiler. ACM Trans. Program. Lang. Syst. 8(3), 292–325 (1986)
Albert, E., Gomez-Zamalloa, M., Puebla, G.: PET: a partial evaluation-based test case generation tool for Java bytecode. In: ACM SIGPLAN WS on Partial Evaluation and Semantics-based Program Manipulation. ACM Press, New York (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bubel, R., Hähnle, R., Ji, R. (2010). Interleaving Symbolic Execution and Partial Evaluation. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds) Formal Methods for Components and Objects. FMCO 2009. Lecture Notes in Computer Science, vol 6286. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17071-3_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-17071-3_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17070-6
Online ISBN: 978-3-642-17071-3
eBook Packages: Computer ScienceComputer Science (R0)