Treffer: Termination graphs for Java Bytecode
Title:
Termination graphs for Java Bytecode
Authors:
Contributors:
The Pennsylvania State University CiteSeerX Archives
Publication Year:
2010
Collection:
CiteSeerX
Document Type:
Fachzeitschrift
text
File Description:
application/pdf
Language:
English
Availability:
Rights:
Metadata may be used without restrictions as long as the oai identifier remains attached to it.
Accession Number:
edsbas.AC47A596
Database:
BASE
Weitere Informationen
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. 1