My research activities concern the static analysis by
abstract interpretation of programs.
In particular, I
am interested in the verification of hybrid systems written
in Matlab/Simulink and numerical properties such as
During my PhD thesis, I defined a static analysis of
offers a convenient way to model and to simulate embedded
systems that is embedded software and its physical
Applying formal verification on Simulink
models allows to validate embedded software taking into
account a model of their execution environment.
During my ATER, I am working with
Didier on the definition of a method to automatically
transform floating-point programs into fixed-point
equivalent ones. We focus our work on Simulink models.
List of my publications on HAL
Some accepted publication
I used to be a PhD student under the supervision of
Matthieu Martel in the laboratory MeASI at
Have a look at my PhD thesis (in French):
"Simulation abstraite : une analyse statique de
- 2013/04/22, Séminaire COMMANDS
Calcul d'ensemble de trajectoires de systèmes hybrides par des méthodes numériques garanties
- 2011/12/01, Workshop
An operational semantics of the simulation engine of
Projects and Collaborations
I am participating in the
ANR INS CAFEIN project.
I visited Walid
Taha for 5 weeks in September 2009 at Rice
University. I implemented a pretty-printer for a new DSL
dedicated to cyber-physical systems
named Acumen. I
also worked on the exact real arithmetic with him and his
I worked with Knowledge
Inside on the transformation of floating-point
programs into fixed-point programs.
During my PhD thesis, I was involved in the project
The aim of this project is to bring formal methods
into the cycle of developement of the embedded systems in
I took part in the
first OCaml Summer
Project organized by
The goal of this project was the
developement of a mathematical library written in
combining numerical and symbolic algorithms.
This work was carried out
Bouissou. The source code of the project can be
found on the
My teachings in computer science are made at
In particular, I teach
I am involved in the development of
library. It aims at solving ordinary differential equations
with validated Runge-Kutta methods.
For the community:
for this web page style.