Program Specialization via a Software Verification Tool

  • Richard Bubel
  • Reiner Hähnle
  • Ran Ji
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6957)


Partial evaluation is a program specialization technique that allows to optimize a program for which partial input is known. We propose a new approach to generate specialized programs for a Java-like language via the software verification tool KeY. This is achieved by symbolically executing source programs interleaved with calls to a simple partial evaluator. In a second phase the specialized programs are synthesized from the symbolic execution tree. The correctness of this approach is guaranteed by a bisimulation relation on the source and specialized programs.


Specialized Program Partial Evaluation Variable Assignment Program Variable Sequent Calculus 
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.


  1. 1.
    Augustsson, L.: A compiler for lazy ML. In: Proceedings of the 1984 ACM Symposium on LISP and functional programming, LFP 1984, pp. 218–227. ACM, New York (1984)CrossRefGoogle Scholar
  2. 2.
    Barrett, C.W., Fang, Y., Goldberg, B., Hu, Y., Pnueli, A., Zuck, L.D.: TVOC: A translation validator for optimizing compilers. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 291–295. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  3. 3.
    Beckert, B., Hähnle, R., Schmitt, P. (eds.): Verification of Object-Oriented Software. The KeY Approach. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)Google Scholar
  4. 4.
    Breebaart, L.: Rule-based compilation of data parallel programs. PhD thesis, Delft University of Technology (2003)Google Scholar
  5. 5.
    Bubel, R., Hähnle, R., Ji, R.: Interleaving symbolic execution and partial evaluation. In: de Boer, F.S., Bonsangue, M.M., Hallerstede, S., Leuschel, M. (eds.) FMCO 2009. LNCS, vol. 6286, pp. 125–146. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  6. 6.
    Clarke, D., Diakov, N., Hähnle, R., Johnsen, E.B., Schaefer, I., Schäfer, J., Schlatte, R., Wong, P.Y.H.: Modeling spatial and temporal variability with the HATS abstract behavioral modeling language. In: Bernardo, M., Issarny, V. (eds.) SFM 2011. LNCS, vol. 6659, pp. 417–457. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  7. 7.
    Clarke, D., Muschevici, R., Proença, J., Schaefer, I., Schlatte, R.: Variability modelling in the ABS language. In: Aichernig, B.K., de Boer, F.S., Bonsange, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 206–226. Springer, Heidelberg (2011)Google Scholar
  8. 8.
    Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes 28, 2 (2003)CrossRefGoogle Scholar
  9. 9.
    Harel, D., Kozen, D., Tiuryn, J.: Dynamic Logic. MIT Press, Cambridge (2000)zbMATHGoogle Scholar
  10. 10.
    Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10) (October 1969)Google Scholar
  11. 11.
    Hoare, T.: The verifying compiler: A grand challenge for computing research. J. ACM 50, 63–69 (2003)CrossRefzbMATHGoogle Scholar
  12. 12.
    Jones, N., Gomard, C., Sestoft, P.: Partial Evaluation and Automatic Program Generation. Prentice Hall, New York (1993)zbMATHGoogle Scholar
  13. 13.
    King, J.C.: A program verifier. PhD thesis, Carnegie-Mellon University (1969)Google Scholar
  14. 14.
    Ruf, E.S.: Topics in online partial evaluation. PhD thesis, Stanford University, Stanford, CA, USA, UMI Order No. GAX93-26550 (1993)Google Scholar
  15. 15.
    Schultz, U.P., Lawall, J.L., Consel, C.: Automatic program specialization for Java. ACM Trans. Program. Lang. Syst. 25(4), 452–499 (2003)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Richard Bubel
    • 1
  • Reiner Hähnle
    • 1
  • Ran Ji
    • 1
  1. 1.Department of Computer Science and EngineeringChalmers University of TechnologyGothenburgSweden

Personalised recommendations