 |
 |
 |
Conference papers
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.
Keywords :
1998 ACM Subject Classification D24 Software/Program Verification (Formal methods)
F31 Specifying and Verifying and Reasoning about Programs (Mechanical verification)
F32 Se-mantics of Programming Languages (Program analysis) Keywords and phrases Non-Termination
Android
Dalvik
Constraint Logic Programming
Cited literature [7 references]
https://hal.univ-reunion.fr/hal-01451692
Contributor : Réunion Univ Connect in order to contact the contributor
Submitted on : Friday, November 9, 2018 - 8:50:36 AM
Last modification on : Friday, January 21, 2022 - 3:27:02 AM
Long-term archiving on: : Sunday, February 10, 2019 - 12:47:43 PM
Contributor : Réunion Univ Connect in order to contact the contributor
Submitted on : Friday, November 9, 2018 - 8:50:36 AM
Last modification on : Friday, January 21, 2022 - 3:27:02 AM
Long-term archiving on: : Sunday, February 10, 2019 - 12:47:43 PM