Interpretation-based value analysis is a classical approach for verifying programs with floating-point computations. However, state-of-the-art tools compute an over-approximation of the variable values that can be very coarse. Constraint solvers have recently been used to significantly refine the approximations computed by such tools. In this paper, we introduce a hybrid approach that combines abstract interpretation and constraint programming techniques in a single static and automatic analysis. First experiments showed that this approach can successfully analyze programs that could not be handled by abstract interpretation or constraint programming tools alone.

Loop invariants play a major role in program verification. Though various techniques have been applied to automatic loop invariants generation, most interesting ones often generate only candidate invariants. Thus, a key issue to take advantage of these invariants in a verification process is to check that these candidate loop invariants are actual invariants. This paper introduces a new technique based on constraint programming for automatic verification of inductive loop invariants. This approach is efficient to detect spurious invariants and is also able to verify valid invariants under boundedness restrictions. First experiments on classical benchmarks are very promising.

Numerous approaches have been proposed for path planning in dynamic current fields, for a fixed departure time. However, in many applications, the departure time is not necessarily known in advance, but can vary in a time window. In this context, the choice of a good departure time is a critical issue. That is why we introduce in this paper a new approach, called symbolic wavefront expansion, determining both the path and the departure time minimizing the travel time of the vehicle. The key idea of this approach is to propagate and compose functions instead of numerical values, with appropriate operators.

The wavefront expansion is commonly used for path planning tasks and appreciated for its efficiency. However, the existing extensions able to handle currents are subject to incorrectness and incompleteness issues when these currents become strong. That is, they may return physically infeasible paths or no path at all, even if a feasible path exists. This behavior endangers the robot, especially in a dynamic replanning context. That is why we propose a new extension called sliding wavefront expansion. This algorithm, combining an appropriate cost function and continuous optimization techniques, guarantees the existence of a path with an arbitrary precision.

Automatic test data generation leads to identify input values on which a selected point in a procedure is executed. This paper introduces a new method for this problem based on constraint solving techniques. First, we statically transform a procedure into a constraint system by using well-known "Static Single Assignment" form and control-dependencies. Second, we solve this system to check whether at least one feasible control flow path going through the selected point exists and to generate test data that correspond to one of these paths.The key point of our approach is to take advantage of current advances in constraint techniques when solving the generated constraint system. Global constraints are used in a preliminary step to detect some of the non feasible paths. Partial consistency techniques are employed to reduce the domains of possible values of the test data. A prototype implementation has been developped on a restricted subset of the C language. Advantages of our approach are illustrated on a non-trivial example.

In this paper we introduce a multi-solver approach for solving systems of constraints over the reals. First, we informally show how a cooperation between different solvers makes it possible to solve problems that none of these solvers can tackle alone. Then, we specify a cooperative architecture based upon agents that communicate via asynchronous message passing. This architecture allows to use concurrently symbolic and numerical solvers together, in order to handle constraints over the real numbers.>

Abstract This paper explores PrologIII's capabilities through the study of two short but non‐trivial applications that are chosen to show the advantages of constraint logic programming languages over conventional Prologs, especially for tackling combinatorial problems. The first application (manipulation of causal graphs) highlights the expressive power of the constraints on booleans and shows that constraint logic programming techniques provide great flexibility for the exploration of the domain of an application, and therefore significantly improve Prolog's prototyping capabilities. The second application (map colouring) demonstrates that a combined use of numerical constraints and constraints on trees of PrologIII enables one to improve solutions based on standard backtracking, through the use of simple heuristics. Such heuristics allow drastic reduction of the search space and yield good performance even for quite complex problems. The adaptability of the approach to other combinatorial problems is shown on several examples.