Research Activities
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
numerical precision.
During my PhD thesis, I defined a static analysis of
Simulink models
[7,5].
Simulink
offers a convenient way to model and to simulate embedded
systems that is embedded software and its physical
environment.
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
Laurent-Stéphane
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.
PhD students
- (2021-2024) I am co-supervising
with Goran Frehse
the PhD thesis
of Danil Berrah.
- (2021-2024) I am co-supervising
with Olivier Doaré
the PhD thesis
of Caroline Pascal.
- (2019-2022) I co-supervised
with Goran Frehse, Bruno Hérissé and Julien Alexandre dit Sandretto
the PhD thesis
of Etienne Bertin.
- (2016-2019) I co-supervised
with Sylvie
Boldo the PhD thesis
of Florian
Faissole.
- (2014-2017) I co-supervised
with
Matthieu Martel the Phd thesis
of Nasrine
Damouche.
- (2012--2017) I co-supervised
with
Michel
Kieffer and
Olivier Bouissou the PhD thesis of Adel Djaballah.
Publications
List of my publications on HAL
Projects and Collaborations
-
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
students.
-
I took part in the
first OCaml Summer
Project organized by
Jane Street
Captial.
The goal of this project was the
developement of a mathematical library written in
OCaml
combining numerical and symbolic algorithms.
This work was carried out
with Olivier
Bouissou. The source code of the project can be
found on the
Sourceforge server.
Teaching Activities
My teachings in computer science are mostly made at
ENSTA Paris.
See the list of my courses
DynIbex software
I am involved in the development of
the DynIbex
library. It aims at solving ordinary differential equations
with validated Runge-Kutta methods.
Various
For the community:
Thanks
Hugo Gimbert
for this web page style.