Non-termination of Dalvik bytecode via compilation to CLP

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.
Document type :
Conference papers
Complete list of metadatas

Cited literature [7 references]  Display  Hide  Download

http://hal.univ-reunion.fr/hal-01451692
Contributor : Réunion Univ <>
Submitted on : Friday, November 9, 2018 - 8:50:36 AM
Last modification on : Thursday, March 28, 2019 - 11:24:10 AM
Long-term archiving on : Sunday, February 10, 2019 - 12:47:43 PM

Identifiers

  • HAL Id : hal-01451692, version 1

Collections

Citation

Etienne Payet, Frédéric Mesnard. Non-termination of Dalvik bytecode via compilation to CLP. 14th International Workshop on Termination (WST), Jul 2014, Vienne, Austria. pp.65-69. ⟨hal-01451692⟩

Share

Metrics

Record views

16

Files downloads

8