Abstract

We revisit termination graphs from the viewpoint of runtime complexity. Suitably generalising the construction proposed in the literature, we define an alternative representation of Jinja Bytecode (JBC) executions as computation graphs. We show that the transformation from JBC programs to computation graphs is sound, i.e., an infinite execution gives rise to an infinite path in the computation graph. Moreover, we establish that the transformation is complexity preserving.

BibTeX

@inproceedings{MS-WST12,
  author    = "Georg Moser and Michael Schaper",
  title     = "Termination Graphs Revisited",
  booktitle = "Proceedings of the 12th International Workshop on Termination (WST 2012)",
  pages     = "64--68",
  year      = 2012
}