2 citations · 6 across the 12 of their papers we have counts for
Showing 2014Show all
3 papers · 1 filter
cs.PL2014
Non-termination of Dalvik bytecode via compilation to CLP
Etienne Payet, Fred Mesnard
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…
cs.LO2014
A Second-Order Formulation of Non-Termination
Fred Mesnard, Etienne Payet
We consider the termination/non-termination property of a class of loops. Such loops are commonly used abstractions of real program pieces. Second-order logic is a convenient langu…
cs.PL2014★ 2 cited
Non-Termination Analysis of Java Bytecode
Étienne Payet, Fred Mesnard, Fausto Spoto
We introduce a fully automated static analysis that takes a sequential Java bytecode program P as input and attempts to prove that there exists an infinite execution of P. The tech…