2014/12/10 by Étienne Payet, Etienne Payet, Fred Mesnard +2
Computer Science · Mathematics · #Bytecode #Computer science #Constraint (computer-aided design) #D.2.4 #F.3.1 #F.3.2 #FOS: Computer and information sciences #Formal Methods in Verification #Logic, Reasoning, and Knowledge #Logic, programming, and type systems #Mathematics #Programming Languages (cs.PL) #Programming language #Set (abstract data type) #Virtual machine #cs.PL
paper · pdf · doi:10.48550/arxiv.1412.3729
5 pages, presented at the 13th International Workshop on Termination (WST) 2013
arxiv created 2014/12/10 · openalex publication_date 2014/12/10 · arxiv updated 2014/12/12 · openalex created_date 2025/10/10 · openalex updated_date 2026/08/05
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.