Non-termination of Dalvik bytecode via compilation to CLP
Programming Languages
2014-12-12 v1
Abstract
We present a set of rules for compiling a Dalvik bytecode program into a logic program with array constraints. Non-termination of the resulting program entails that of the original one, hence the techniques we have presented before for proving non-termination of constraint logic programs can be used for proving non-termination of Dalvik programs.
Keywords
Cite
@article{arxiv.1412.3729,
title = {Non-termination of Dalvik bytecode via compilation to CLP},
author = {Etienne Payet and Fred Mesnard},
journal= {arXiv preprint arXiv:1412.3729},
year = {2014}
}
Comments
5 pages, presented at the 13th International Workshop on Termination (WST) 2013