Non-termination of Dalvik bytecode via compilation to CLP
Résumé
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.
Mots clés
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
Domaines
Informatique [cs]
Fichier principal
Non_termination_of_Dalvik_bytecode_via_compilation_CLP.pdf (388.26 Ko)
Télécharger le fichier
Loading...