Non-termination of Dalvik bytecode via compilation to CLP
Authors: Étienne Payet and Fred Mesnard
Paper Information
| Title: | Non-termination of Dalvik bytecode via compilation to CLP |
| Authors: | Étienne Payet and Fred Mesnard |
| Proceedings: | WST 2014 Informal Proceedings |
| Editor: | Carsten Fuhs |
| Keywords: | Non-Termination, Android, Dalvik, Constraint Logic Programming |
| Abstract: | 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. |
| Pages: | 5 |
| Talk: | Jul 17 08:45 |
| Paper: |  |