Publications

How to make Lisp go faster than C

Didier Verna

Contrary to popular belief, Lisp code can be very efficient today: it can run as fast as equivalent C code or even faster in some cases. In this paper, we explain how to tune Lisp code for performance by introducing the proper type declarations, using the appropriate data structures and compiler information. We also explain how efficiency is achieved by the compilers. These techniques are applied to simple image processing algorithms in order to demonstrate the announced performance on pixel access and arithmetic operations in both languages.

Modeling of sensor networks using XRM

Akim Demaille · Sylvain Peyronnet · Benoît Sigoure

Sensor networks are composed of small electronic devices that embed processors, sensors, batteries, memory and communication capabilities. One of the main goal in the design of such systems is the handling of the inherent complexity of the nodes, strengthened by the huge number of nodes in the network. For these reasons, it becomes very difficult to model and verify such systems. In this paper, we investigate the main characteristics of sensor nodes, discuss about the use of a language derived from Reactive Modules for their modeling and propose a language (and a tool set) that ease the modeling of this kind of systems.

An efficient algorithm for connected attribute thinnings and thickenings

David Lesage · Jérôme Darbon · Ceyhun Burak Akgül

Connected attribute filters are anti-extensive morphological operators widely used for their ability of simplifying the image without moving its contours. In this paper, we present a fast, versatile and easy-to-implement algorithm for grayscale connected attribute thinnings and thickennings, a subclass of connected filters for the wide range of non-increasing attributes. We show that our algorithm consumes less memory and is computationally more efficient than other available methods on natural images.

Evaluating complex MAC protocols for sensor networks with APMC

Michaël Cadilhac · Thomas Hérault · Richard Lassaigne · Sylvain Peyronnet · Sébastien Tixeuil

In this paper we present an analysis of a MAC (Medium Access Control) protocol for wireless sensor networks. The purpose of this protocol is to manage wireless media access by constructing a Time Division Media Access (TDMA) schedule. APMC (Approximate Probabilistic Model Checker) is a tool that uses approximation-based verification techniques in order to analyse the behavior of complex probabilistic systems. Using APMC, we approximately computed the probabilities of several properties of the MAC protocol being studied, thus giving some insights about its performance.

On a polynomial vector field model for shape representation

Mickael Chekroun · Jérôme Darbon · Igor Ciril

In this paper we propose an efficient algorithm to perform a polynomial approximation of the vector field derived from the usual distance mapping method. The main ingredients consist of minimizing a quadratic functional and transforming this problem in an appropriate setting for implementation. With this approach, we reduce the problem of obtaining an approximating polynomial vector field to the resolution of a not expansive linear algebraic system. By this procedure, we obtain an analytical shape representation that relies only on some coefficients. Fidelity and numerical efficiency of our approach are presented on illustrative examples.

Approximate probabilistic model checking for programs

Jérôme Darbon · Richard Lassaigne · Sylvain Peyronnet

In this paper we deal with the problem of applying model checking to real programs. We verify a program without constructing the whole transition system using a technique based on Monte-Carlo sampling, also called “approximate model checking”. This technique combines model checking and randomized approximation. Thus, it avoids the so called state space explosion phenomenon. We propose a prototype implementation that works directly on C source code. It means that, contrary to others approaches, we do not need to use a specific language nor specific data structures in order to describe the system we wish to verify. Finally, we present experimental results that show the effectiveness of the approach applied to finding bugs in real programs.

A note on nice-levelable MRFs for SAR image denoising with contrast preservation

Jérôme Darbon · Marc Sigelle · Florence Tupin

Attribute grammars for modular disambiguation

Valentin David · Akim Demaille · Olivier Gournet

To face the challenges to tomorrow’s software engineering tools, powerful language-generic program-transformation components are needed. We propose the use of attribute grammars (AGs) to generate language specific disambiguation filters. In this paper, a complete implementation of a language-independent AGs system is presented. As a full scale experiment, we present an implementation of a flexible C front-end. Its specifications are concise, modular, and the result is efficient. On top of it, transformations such as software renovation, code metrics, domain specific language embedding can be implemented.

APMC 3.0: Approximate verification of discrete and continuous time Markov chains

Thomas Hérault · Richard Lassaigne · Sylvain Peyronnet

In this paper, we give a brief overview of APMC (Approximate Probabilistic Model Checker). APMC is a model checker that implements approximate probabilistic verification of probabilistic systems. It is based on Monte-Carlo method and the theory of randomized approximation schemes and allows to verify extremely large models without explicitly representing the global transition system. To avoid the state-space explosion phenomenon, APMC gives an accurate approximation of the satisfaction probability of the property instead of the exact value, but using only a very small amount of memory. The version of APMC we present in this paper can now handle efficiently both discrete and continuous time probabilistic systems.

C-Transformers — A framework to write C program transformations

Alexandre Borghi · Valentin David · Akim Demaille

Program transformation techniques have reached a maturity level that allows processing high-level language sources in new ways. Not only do they revolutionize the implementation of compilers and interpreters, but with modularity as a design philosophy, they also permit the seamless extension of the syntax and semantics of existing programming languages. The C-Transformers project provides a transformation environment for C, a language that proves to be hard to transform. We demonstrate the effectiveness of C-Transformers by extending C’s instructions and control flow to support Design by Contract. C-Transformers is developed by members of the LRDE: EPITA undergraduate students.