Software testing is one of the most popular validation techniques in the software industry. Surprisingly, we can only find a few approaches to testing in the context of logic programming. In this paper, we introduce a systematic approach for dynamic
testing that combines both concrete and symbolic execution. Our approach is fully automatic and guarantees full path coverage when it terminates. We prove some basic properties of our technique and illustrate its practical usefulness through a prototype implementation.
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-te
rmination of constraint logic programs can be used for proving non-termination of Dalvik programs.
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 language to express non-termination. Of course, such property is generally
undecidable. However, by restricting the language to known decidable cases, we exhibit new classes of loops, the non-termination of which is decidable. We present a bunch of examples.
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 technique consists in compiling P into a constraint logic program P_CLP an
d in proving non-termination of P_CLP; when P consists of instructions that are exactly compiled into constraints, the non-termination of P_CLP entails that of P. Our approach can handle method calls; to the best of our knowledge, it is the first static approach for Java bytecode able to prove the existence of infinite recursions. We have implemented our technique inside the Julia analyser. We have compared the results of Julia on a set of 113 programs with those provided by AProVE and Invel, the only freely usable non-termination analysers comparable to ours that we are aware of. Only Julia could detect non-termination due to infinite recursion.
