PE-KeY: A Partial Evaluator for Java Programs

  • Ran Ji
  • Richard Bubel
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7321)


We present a prototypical implementation of a partial evaluator for Java programs based on the verification system KeY. We argue that using a program verifier as technological basis provides potential benefits leading to a higher degree of specialization. We discuss in particular how loop invariants and preconditions can be exploited to specialize programs. In addition, we provide the first results which we achieved with the presented tool.


Partial Evaluation Java Program Program Variable Sequent Calculus Proof Obligation 
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.
    Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software. LNCS (LNAI), vol. 4334, pp. 410–451. Springer, Heidelberg (2007)Google Scholar
  2. 2.
    Bubel, R., Hähnle, R., Ji, R.: Program Specialization via a Software Verification Tool. In: Aichernig, B.K., de Boer, F.S., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 80–101. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  3. 3.
    King, J.C.: A program verifier. PhD thesis, CMU (1969)Google Scholar
  4. 4.
    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
  5. 5.
    Schultz, U.P., Lawall, J.L., Consel, C.: Automatic program specialization for Java. ACM-TPLS 25(4), 452–499 (2003)CrossRefGoogle Scholar
  6. 6.
    Shali, A., Cook, W.R.: Hybrid partial evaluation. In: OOPSLA, pp. 375–390 (2011)Google Scholar
  7. 7.
    Ruf, E.S.: Topics in online partial evaluation. PhD thesis, Stanford University, Stanford, CA, USA, UMI Order No. GAX93-26550 (1993)Google Scholar
  8. 8.
    Hatcliff, J.: Mechanically Verifying the Correctness of an Offline Partial Evaluator. In: Swierstra, S.D. (ed.) PLILP 1995. LNCS, vol. 982, pp. 279–298. Springer, Heidelberg (1995)CrossRefGoogle Scholar
  9. 9.
    Hatcliff, J., Danvy, O.: A computational formalization for partial evaluation. Mathematical Structures in Computer Science 7(5), 507–541 (1997)MathSciNetzbMATHCrossRefGoogle Scholar
  10. 10.
    Hoare, T.: The verifying compiler: A grand challenge for computing research. J. ACM 50, 63–69 (2003)CrossRefGoogle Scholar
  11. 11.
    Dave, M.A.: Compiler verification: a bibliography. SIGSOFT Softw. Eng. Notes 28, 2 (2003)CrossRefGoogle Scholar
  12. 12.
    Augustsson, L.: A compiler for lazy ML. In: Proc. of the ACM Symposium LFP 1984, pp. 218–227. ACM, New York (1984)CrossRefGoogle Scholar
  13. 13.
    Breebaart, L.: Rule-based compilation of data parallel programs. PhD thesis, Delft University of Technology (2003)Google Scholar
  14. 14.
    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
  15. 15.
    Stärk, R.F., Schmid, J., Börger, E.: Java and the Java Virtual Machine. Springer (2001)Google Scholar
  16. 16.
    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
  17. 17.
    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., Bonsangue, M.M. (eds.) FMCO 2010. LNCS, vol. 6957, pp. 204–224. Springer, Heidelberg (2011)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Ran Ji
    • 1
  • Richard Bubel
    • 1
  1. 1.Technische Universität DarmstadtGermany

Personalised recommendations