We present abstract acceleration techniques for computing loop invariants for numerical programs with linear assignments and conditionals. Whereas abstract interpretation techniques typically over-approximate the set of reachable states iteratively, abstract acceleration captures the effect of the loop with a single, non-iterative transfer function applied to the initial states at the loop head. In contrast to previous acceleration techniques, our approach applies to any linear loop without restrictions. Its novelty lies in the use of the Jordan normal form decomposition of the loop body to derive symbolic expressions for the entries of the matrix modeling the effect of η ≥ Ο iterations of the loop. The entries of such a matrix depend on η through complex polynomial, exponential and trigonometric functions. Therefore, we introduces an abstract domain for matrices that captures the linear inequality relations between these complex expressions. This results in an abstract matrix for describing the fixpoint semantics of the loop.

Hybrid systems are used to model embedded computing systems interacting with their physical environment. There is a conceptual mismatch between high-level hybrid system languages like Simulink, which are used for simulation, and hybrid automata, the most suitable representation for safety verification. Indeed, in simulation languages the interaction between discrete and continuous execution steps is specified using the concept of zero-crossings, whereas hybrid automata exploit the notion of staying conditions. We describe a translation from a hybrid data-flow language to logico-numerical hybrid automata that points out this issue carefully. We expose various zero-crossing semantics, propose a sound translation, and discuss to which extent the original semantics is preserved.

This paper addresses the verification of hybrid systems built as the composition of a discrete software controller interacting with a physical environment exhibiting a continuous behavior. The goal is to attack the problem of the combinatorial explosion of discrete states that may happen if a complex software controller is considered. It proposes as a solution to extend an existing abstract interpretation technique, namely dynamic partitioning, to hybrid systems described in a symbolic formalism. Dynamic partitioning allows us finely tune the tradeoff between precision and efficiency in a reachability analysis. It shows the effectiveness of the approach by a case study that combines a nontrivial controller specified in the synchronous dataflow programming language Lustre with its physical environment.

This article addresses the verification of properties of imperative programs with recursive procedure calls, heap-allocated storage, and destructive updating of pointer-valued fields, that is, interprocedural shape analysis . The article makes three contributions. — It introduces a new method for abstracting relations over memory configurations for use in abstract interpretation. — It shows how this method furnishes the elements needed for a compositional approach to shape analysis. In particular, abstracted relations are used to represent the shape transformation performed by a sequence of operations, and an overapproximation to relational composition can be performed using the meet operation of the domain of abstracted relations. — It applies these ideas in a new algorithm for context-sensitive interprocedural shape analysis. The algorithm creates procedure summaries using abstracted relations over memory configurations, and the meet-based composition operation provides a way to apply the summary transformer for a procedure P at each call site from which P is called. The algorithm has been applied successfully to establish properties of both (i) recursive programs that manipulate lists and (ii) recursive programs that manipulate binary trees.

We address the verification of hybrid systems built as the composition of a discrete software controller interacting with a physical environment exhibiting a continuous behavior. Our goal is to attack the problem of the combinatorial explosion of discrete states that may happen if a complex software controller is considered. We propose as a solution to extend an existing abstract interpretation technique, namely dynamic partitioning, to hybrid systems described in a symbolic formalism. Dynamic partitioning allows to finely tune the tradeoff between precision and efficiency in the analysis. We show the effectiveness of the approach by a case study that combines a non trivial controller specified in the synchronous dataflow programming language Lustre with its physical environment.

We propose a general analysis method for recursive, concurrent programs that tracks effectively procedure calls and returns in a concurrent context, even in the presence of unbounded recursion and infinite-state variables like integers. This method generalizes the relational interprocedural analysis of sequential programs to the concurrent case. We implemented it for programs with scalar variables, and we experimented several classical synchronisation protocols in order to illustrate the precision of our technique, but also to analyze the approximations it performs.

This paper presents a technique to map automatically a complete digital signal processing (DSP) application onto a parallel machine with distributed memory. Unlike other applications where coarse or medium grain scheduling techniques can be used, DSP applications integrate several thousand of tasks and hence necessitate fine grain considerations. Moreover finding an effective mapping imperatively require to take into account both architectural resources constraints and real time constraints. The main contribution of this paper is to show how it is possible to handle and to solve data partitioning, and fine-grain scheduling under the above operational constraints using concurrent constraints logic programming languages (CCLP). Our concurrent resolution technique undertaking linear and nonlinear constraints takes advantage of the special features of signal processing applications and provides a solution equivalent to a manual solution for the representative panoramic analysis (PA) application.