Non-termination of Dalvik bytecode via compilation to CLP

Etienne Payet; Frédéric Mesnard

Non-termination of Dalvik bytecode via compilation to CLP

Etienne Payet ¹ Frédéric Mesnard ¹

1 LIM - Laboratoire d'Informatique et de Mathématiques

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 : Constraint Logic Programming Android Dalvik F32 Se-mantics of Programming Languages (Program analysis) Keywords and phrases Non-Termination F31 Specifying and Verifying and Reasoning about Programs (Mechanical verification) 1998 ACM Subject Classification D24 Software/Program Verification (Formal methods)

Document type :

Conference papers

Domain :

Computer Science [cs]

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

Non-termination of Dalvik bytecode via compilation to CLP

File

Identifiers

Collections

Citation

Export

Metrics

16

8

Contact

Non-termination of Dalvik bytecode via compilation to CLP

File

Identifiers

Collections

Citation

Export

Share

Metrics

16

8

Contact