2^nd years: graphical interfaces with AWT/Swing, network-oriented developments in C and Java, network administration under Linux.

3^rd years and post graduate degrees (DESS) in CS: advanced C++.

3^rd years and PhD (DEA): synchronous reactive development (Esterel, Lustre).

Degree (DEUG) in CS and Math: Programming, Algorithms and Data Structures, Functional Programming.

Bachelor's Degree (Licence) in CS: Advanced Functional Programming.

Master's Degree (Maîtrise) in CS: Advanced C++.

"Implicit and explicit exploration of the reachable state space of Esterel logical circuits"

Esterel is a language aimed at modeling concurrent, reactive and synchronous systems that communicates through instantaneous broadcasting of signals. Besides usual language constructs, Esterel offers constructs for parallelization, sequencing, preemption, suspension, escaping, instantaneous broadcast of signals, signal waiting, etc. At the heart of the compiler, programs are represented by logical circuits. From there, Esterel programs can be executed by regular processors through the C back-end or they can be converted into integrated circuits, through the VHDL back-end.

The Esterel language is based upon the Finite State Machine (FSM) semantic model. Therefore, the reachable state space of programs can be explored. These reachable state spaces can be explored in a symbolic way, for instance by using Binary Decision Diagrams (BDDs), or explicitly enumerated. However, RSS computations have an exponential complexity in the worst case. I have developed several techniques aiming at reducing the costs of these RSS computations and avoiding as much as possible explosions in time and/or space.

In the framework of implicit techniques (based upon BDDs), I have developed a method that allows to abstract some of the variables involved in computations using a tri-valued logic. This technique, when properly used, allows to drastically reduce the cost of reachable state space computations, both in time and space, at the price of an over-approximation of the result. This technique has been applied in a formal verifier of safety properties.

In the framework of explicit techniques (based upon enumerations), I have developped a new reachable state space exploration engine. This new engine is more efficient that the older one by several orders of magnitude. This engine has lead to a new automaton generation tool which has been included in the Esterel compiler, integrated within the Esterel Studio integrated development environment, marketed by Esterel Technologies Inc.. This new engine has also been applied to exhaustive test sequence generation and appeared to be much more efficient than a similar tool based upon BDDs. Eventually, this engine has also lead to a formal verifier of safety properties and appeared to be very efficient on models with a strongly linear behavior, on which BDD-based or SAT-based verifiers failed.

End of year project: a development environment for DSPs that checks bus access conflicts.