Fred Mesnard
LPTP (Logic Program Theorem Prover) is an interactive natural-deduction-based theorem prover for pure Prolog programs with negation as failure, unification with the occurs check, and a restricted but extensible set of built-in predicates.…
This report contains the proceedings of the 19th International Workshop on Termination (WST 2023), which was held in Obergurgl during August 24--25 as part of Obergurgl Summer on Rewriting (OSR 2023).
Concolic testing is a popular software verification technique based on a combination of concrete and symbolic execution. Its main focus is finding bugs and generating test cases with the aim of maximizing code coverage. A previous approach…
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…
Concolic testing mixes symbolic and concrete execution to generate test cases covering paths effectively. Its benefits have been demonstrated for more than 15 years to test imperative programs. Other programming paradigms, like logic…
This volume constitutes the pre-proceedings of the 28th International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2018), held on 4-6th September 2018 in Frankfurt am Main, Germany and co-located with the 20th…
Concolic testing is a popular dynamic validation technique that can be used for both model checking and automatic test case generation. We have recently introduced concolic testing in the context of logic programming. In contrast to…
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…
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…
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 termination is a hot research topic in program analysis. The last few years have witnessed the development of termination analyzers for programming languages such as C and Java with remarkable precision and performance. These…
The classical technique for proving termination of a generic sequential computer program involves the synthesis of a ranking function for each loop of the program. Linear ranking functions are particularly interesting because many…
On the one hand, termination analysis of logic programs is now a fairly established research topic within the logic programming community. On the other hand, non-termination analysis seems to remain a much less attractive subject. If we…
In this paper we introduce a class of constraint logic programs such that their termination can be proved by using affine level mappings. We show that membership to this class is decidable in polynomial time.
On one hand, termination analysis of logic programs is now a fairly established research topic within the logic programming community. On the other hand, non-termination analysis seems to remain a much less attractive subject. If we divide…
We present a static analysis technique for non-termination inference of logic programs. Our framework relies on an extension of the subsumption test, where some specific argument positions can be instantiated while others are generalized.…
A programming tactic involving polyhedra is reported that has been widely applied in the polyhedral analysis of (constraint) logic programs. The method enables the computations of convex hulls that are required for polyhedral analysis to be…
We present cTI, the first system for universal left-termination inference of logic programs. Termination inference generalizes termination analysis and checking. Traditionally, a termination analyzer tries to prove that a given class of…
Since the seminal work of J. A. Robinson on resolution, many lifting lemmas for simplifying proofs of completeness of resolution have been proposed in the literature. In the logic programming framework, they may also help to detect some…