Abstract
To prove termination of Java Bytecode (JBC) automatically, we transform JBC to finite termination graphs which represent all possible runs of the program. Afterwards, the graph can be translated into “simple” formalisms like term rewriting and existing tools can be used to prove termination of the resulting term rewrite system (TRS). In this paper we show that termination graphs indeed capture the semantics of JBC correctly. Hence, termination of the TRS resulting from the termination graph implies termination of the original JBC program.
Supported by the DFG grant GI 274/5-3 and by the G.I.F. grant 966-116.6.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Albert, E., Arenas, P., Codish, M., Genaim, S., Puebla, G., Zanardini, D.: Termination analysis of Java Bytecode. In: Barthe, G., de Boer, F.S. (eds.) FMOODS 2008. LNCS, vol. 5051, pp. 2–18. Springer, Heidelberg (2008)
Berdine, J., Cook, B., Distefano, D., O’Hearn, P.: Automatic termination proofs for programs with shape-shifting heaps. In: Ball, T., Jones, R.B. (eds.) CAV 2006. LNCS, vol. 4144, pp. 386–400. Springer, Heidelberg (2006)
Brockschmidt, M., Otto, C., von Essen, C., Giesl, J.: Termination graphs for Java Bytecode. Technical Report AIB-2010-15, RWTH Aachen (2010), http://aib.informatik.rwth-aachen.de
Colón, M., Sipma, H.: Practical methods for proving program termination. In: Brinksma, E., Larsen, K.G. (eds.) CAV 2002. LNCS, vol. 2404, pp. 442–454. Springer, Heidelberg (2002)
Cook, B., Podelski, A., Rybalchenko, A.: Termination proofs for systems code. In: Schwartzbach, M.I., Ball, T. (eds.) PLDI 2006, pp. 415–426. ACM Press, New York (2006)
Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: Proc. POPL 1977, pp. 238–252. ACM Press, New York (1977)
De Schreye, D., Decorte, S.: Termination of logic programs: The never-ending story. Journal of Logic Programming 19-20, 199–260 (1994)
Dershowitz, N.: Termination of rewriting. J. Symb. Comp. 3(1-2), 69–116 (1987)
Fuhs, C., Giesl, J., Plücker, M., Schneider-Kamp, P., Falke, S.: Proving termination of integer term rewriting. In: Treinen, R. (ed.) RTA 2009. LNCS, vol. 5595, pp. 32–47. Springer, Heidelberg (2009)
Giesl, J., Raffelsieper, M., Schneider-Kamp, P., Swiderski, S., Thiemann, R.: Automated termination proofs for Haskell by term rewriting. ACM TOPLAS (to appear)
Giesl, J., Schneider-Kamp, P., Thiemann, R.: AProVE 1.2: Automatic termination proofs in the DP framework. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 281–286. Springer, Heidelberg (2006)
Klein, G., Nipkow, T.: A machine-checked model for a Java-like language, virtual machine and compiler. ACM TOPLAS 28(4), 619–695 (2006)
Lindholm, T., Yellin, F.: Java Virtual Machine Specification. Prentice-Hall, Englewood Cliffs (1999)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL — A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)
Otto, C., Brockschmidt, M., von Essen, C., Giesl, J.: Automated termination analysis of Java Bytecode by term rewriting. In: Lynch, C. (ed.) RTA 2010. LIPIcs, vol. 6, pp. 259–276. Dagstuhl Publishing (2010)
Schneider-Kamp, P., Giesl, J., Serebrenik, A., Thiemann, R.: Automated termination proofs for logic programs by term rewriting. ACM TOCL 11(1) (2009)
Sørensen, M.H., Glück, R.: An algorithm of generalization in positive supercompilation. In: Lloyd, J.W. (ed.) ILPS 1995, pp. 465–479. MIT Press, Cambridge (1995)
Spoto, F., Mesnard, F., Payet, É.: A termination analyser for Java Bytecode based on path-length. ACM TOPLAS 32(3) (2010)
Walther, C.: Mathematical induction. In: Handbook of Logic in Artificial Intelligence and Logic Programming, vol. 2, pp. 127–227. Oxford University Press, Oxford (1994)
Walther, C.: On proving the termination of algorithms by machine. Artificial Intelligence 71(1), 101–157 (1994)
Walther, C.: Semantik und Programmverifikation. Teubner-Wiley, Chichester (2001)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Brockschmidt, M., Otto, C., von Essen, C., Giesl, J. (2010). Termination Graphs for Java Bytecode . In: Siegler, S., Wasser, N. (eds) Verification, Induction, Termination Analysis. Lecture Notes in Computer Science(), vol 6463. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17172-7_2
Download citation
DOI: https://doi.org/10.1007/978-3-642-17172-7_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17171-0
Online ISBN: 978-3-642-17172-7
eBook Packages: Computer ScienceComputer Science (R0)