Concolic testing is a well-known validation technique for imperative and object oriented programs. In a previous paper, we have introduced an adaptation of this technique to logic programming. At the heart of our framework lies a specific procedure that we call “selective unification”. It is used to generate appropriate run-time goals by considering all possible ways an atom can unify with the heads of some program clauses. In this paper, we show that the existing algorithm for selective unification is not complete in the presence of non-linear atoms. We then prove soundness and completeness for a restricted version of the problem where some atoms are required to be linear. We also consider concolic testing in the context of constraint logic programming and extend the notion of selective unification accordingly.

Abstract 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 to concolic testing in logic programming was not sound because it only dealt with positive constraints (by means of substitutions) but could not represent negative constraints. In this paper, we present a novel framework for concolic testing of CLP programs that generalizes the previous technique. In the CLP setting, one can represent both positive and negative constraints in a natural way, thus giving rise to a sound and (potentially) more efficient technique. Defining verification and testing techniques for CLP programs is increasingly relevant since this framework is becoming popular as an intermediate representation to analyze programs written in other programming paradigms.

Concolic testing is a well-known validation technique for imperative and object-oriented programs. We have recently introduced an adaptation of this technique to logic programming. At the heart of our framework for concolic testing lies a logic programming specific procedure that we call "selective unification". In this paper, we consider concolic testing in the context of constraint logic programming and extend the notion of selective unification accordingly. We prove that the selective unification problem is generally undecidable for constraint logic programs, and we present a correct and complete algorithm for selective unification in the context of a class of constraint structures.

Algorithm recognition, which is the problem of verifying whether a program implements a given algorithm, is an important topic in program analysis. We propose an approach for algorithm recognition in binary code. For this paper, we have chosen the Dalvik Virtual Machine (DVM) bytecode. Given an algorithm A that is compiled into a DVM method M0, and a DVM program P that includes a series of methods {M1,..., Mn}, the approach is able to identify those blocks Mi from P that essentially implement the algorithm A. The technique we propose first translates binary code into Horn clauses. Then we consider programs as implementing the same algorithm if their Horn clause representations can be reduced to a single common set of Horn clauses by means of a sequence of transformations.

Abstract 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.

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 systems are largely based on techniques and tools coming from the field of declarative constraint programming. In this paper, we first recall an algorithm based on Farkas' Lemma for discovering linear ranking functions proving termination of a certain class of loops. Then we propose an extension of this method for showing the existence of eventual linear ranking functions, i.e., linear functions that become ranking functions after a finite unrolling of the loop. We show correctness and completeness of this algorithm.

Most civil aviation aircraft are equipped with meteorological radar working at the X-band (f≈ 10 GHz; λ ≈ 3.2 cm) . These radars use a small antenna and, thus, a large beamwidth, around 3°-4°, for observations over long distances (up to 350 km). In the presence of microphysical inhomogeneities inside a radar sampling volume, as filling by different hydrometeor categories, radar reflectivity measurements are biased. An important bias occurs when a radar cell is cut by a nonresolved layer of melting snowflakes whose attenuation is high compared to those of rain and dry snow. This paper illustrates the effects in precipitation-attenuation correction schemes (PACS) of the inhomogeneity associated with the 0 °C isotherm. It proposes a method to take into account these effects in PACS. Adaptation of the method to other frequency bands and ground-based radar observations is easy.

We present a type system for linear constraints over the reals intended for reasoning about the input-output directionality of variables. Types model the properties of definiteness, range width or approximation, lower and upper bounds of variables in a linear constraint. Several proof procedures are presented for inferring the type of a variable and for checking validity of type assertions. We rely on theory and tools for linear programming problems, linear algebra, parameterized polyhedra and negative constraints. An application of the type system is proposed in the context of the static analysis of constraint logic programs. Type assertions are at the basis of the extension of well-moding from pure logic programming. The proof procedures (both for type assertion validity and for well-moding) are implemented and their computational complexity is discussed. We report experimental results demonstrating the efficiency in practice of the proposed approach.

It is important to prove that supposedly terminating programs actually terminate, particularly if those programs must be run on critical systems or downloaded into a client such as a mobile phone. Although termination of computer programs is generally undecidable, it is possible and useful to prove termination of a large, nontrivial subset of the terminating programs. In this article, we present our termination analyzer for sequential Java bytecode, based on a program property called path-length . We describe the analyses which are needed before the path-length can be computed such as sharing, cyclicity, and aliasing. Then we formally define the path-length analysis and prove it correct with respect to a reference denotational semantics of the bytecode. We show that a constraint logic program P CLP can be built from the result of the path-length analysis of a Java bytecode program P and formally prove that if P CLP terminates, then P also terminates. Hence a termination prover for constraint logic programs can be applied to prove the termination of P . We conclude with some discussion of the possibilities and limitations of our approach. Ours is the first existing termination analyzer for Java bytecode dealing with any kind of data structures dynamically allocated on the heap and which does not require any help or annotation on the part of the user.

Abstract 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 divide this line of research into two kinds of approaches, dynamic versus static analysis, this paper belongs to the latter. It proposes a criterion for detecting non-terminating atomic queries with respect to binary constraint logic programming (CLP) rules, which strictly generalizes our previous works on this subject. We give a generic operational definition and an implemented logical form of this criterion. Then we show that the logical form is correct and complete with respect to the operational definition.

Abstract 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.

We present a static analysis technique for nontermination 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. We give syntactic criteria to statically identify such argument positions from the text of a program. Atomic left looping queries are generated bottom-up from selected subsets of the binary unfoldings of the program of interest. We propose a set of correct algorithms for automating the approach. Then, nontermination inference is tailored to attempt proofs of optimality of left termination conditions computed by a termination inference tool. An experimental evaluation is reported and the analyzers can be tried online at http://www.univ-reunion.fr/~gcc. When termination and nontermination analysis produce complementary results for a logic procedure, then with respect to the leftmost selection rule and the language used to describe sets of atomic queries, each analysis is optimal and together, they induce acharacterizationof the operational behavior of the logic procedure.

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 coded with linear constraint solving machinery that is available in many Prolog systems.

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 queries terminates. This class must be provided to the system, for instance by means of user annotations. Moreover, the analysis must be redone every time the class of queries of interest is updated. Termination inference, in contrast, requires neither user annotations nor recomputation. In this approach, terminating classes for all predicates are inferred at once. We describe the architecture of cTI and report an extensive experimental evaluation of the system covering many classical examples from the logic programming termination literature and several Prolog programs of respectable size and complexity.

The Constraint Logic Programming (CLP) Scheme merges logic programming with constraint solving over predefined domains. In this article, we study proof methods for universal left termination of constraint logic programs. We provide a sound and complete characterization of left termination for ideal CLP languages which generalizesacceptabilityof logic programs. The characterization is then refined to the notion ofpartial acceptability, which is well suited for automatic modular inference. We describe a theoretical framework for automation of the approach, which is implemented. For nonideal CLP languages and without any assumption on their incomplete constraint solvers, even the most basic sound termination criterion from logic programming does not lift. We focus on a specific system, namely CLP(R), by proposing some additional conditions that make (partial) acceptability sound.