---

Research Activities

My research activities concern the static analysis by abstract interpretation of programs.
In particular, I am interested in the verification of 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.

---

Preprints

• [10] Abstract Fixpoint Computations with Numerical Acceleration Methods co-authored with Olivier Bouissou and Yassamine Seladji. Accepted to NSAD'10.
• [9] Interval Slopes as a Numerical Abstract Domain for Floating-Point Variables. Accepted to SAS'10.

---

Publications

You can access to my bibtex file.

• [8] Mathematical Equations as Executable Models co-authored with Yun Zhu, Edwin Westbrook, Jun Inoue, Cherif Salama, Marisa Peralta, Travis Martin, Walid Taha, Marcia O'Malley, Robert Cartwright, Aaron Ames and Raktim Bhattacharya.
  Accepted to ICCPS 2010.
• [7] Abstract Simulation: a Static Analysis of Simulink Models, co-authored with Matthieu Martel.
  Accepted to ICESS 2009. See also the HAL preprint or the published version. [Slides]
• [6] Range Estimation of Floating-Point Variables in Simulink Models , co-authored with Laurent-Stéphane Didier and Fanny Villers.
  Accepted for presentation NSV-II. [Slides]
• [4] Différentiation automatique et formes de Taylor en analyse statique de programmes numériques (in French), co-authored with Matthieu Martel.
  Accepted for Technique et Science Informatique. See also the published version.
• [3] Abstact Simulation: a Static Analysis of Simulink Programs, co-authored with Matthieu Martel.
  Accepted for Model-driven High-level Programming of Embedded Systems (SLA++P'08). Short paper. [Slides]
• [2] Différentiation automatique et formes de Taylor en analyse statique de programmes numériques (in French), co-authored with Matthieu Martel.
  Accepted for Approches Formelles dans l'Assistance au Dévelopement de Logiciels (AFADL'07).
  See the extended version [4].
• [1] Abstract Frequency Analysis of Synchronous Systems , co-authored with Matthieu Martel.
  Accepted for Languages, Compilers and Tools for Embedded Systems (LCTES'06). Poster and short paper.

---

PhD thesis

I used to be a PhD student under the supervision of Matthieu Martel in the laboratory MeASI at CEA Saclay.
Have a look at my PhD thesis (in French): "Simulation abstraite : une analyse statique de modèles Simulink"

• [5] Manuscrit de thèse de doctorat (accessible également sur TEL) et les transparents de la présentation

---

Talks

• 2009/11/30, Séminaire d'équipe, EADS Innovation Works Suresnes
  Transformation du langage LLVM en Newspeak
• 2009/03/13, Séminaire SOC, Laboratoire d'Informatique de Paris 6
  Analyse statique de modèles Simulink - [Slides in French]
• 2008/12/11, Cours interprétation abstraite M2, Univeristé Pierre et Marie Curie
  Analyse statique par interprétation abstraite de programmes numériques : exemple de stage du master LS
• 2008/12/04, Séminaire DALI, Univeristé de Perpignan
  Analyse statique de modèles Simulink
• 2008/06/12, Groupe de travail "Programmation", Laboratoire d'Informatique de Paris 6
  Analyse statique de programmes Simulink - [Slides in French]
• 2008/03/26, Petit Groupe de travail : Modélisation, optimisation et analyse statique, CIRM
  Static analysis of Simulink programs
• 2008/01/24, Cours interprétation abstraite M2, Univeristé Pierre et Marie Curie
  Analyse statique par interprétation abstraite de programmes numériques : exemple de stage du master LS
• 2007/06/7, Séminaire Laboratoire Sûreté des Logiciels, CEA LIST
  Analyse statique fréquentielle de spécifications Simulink
• 2006/12/21, Cours interprétation abstraite M2, Univeristé Pierre et Marie Curie
  Pécision numérique et interprétation abstraite

---

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 work with Knowledge Inside on the transformation of floating-point programs into fixed-point programs.
• During my PhD thesis, I was involved in the project Euréka Syspéo.
  The aim of this project is to bring formal methods into the cycle of developement of the embedded systems in automotive industry.
• 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 made at Polytech'Paris UPMC and University Paris 6 in Computer Science department.

---

CV

My CV is available in french.

---

Various

Some links:

• People: Xavier Allamigeon, Nicolas Ayache, Olivier Bouissou, Michel Hirschowitz, Assalé Adjé
• Software: , APRON, Newspeak

For the community:

• I rewrote the difficult to find but great article of Gilles Kahn "The Semantics of a Simple Language for Parallel Programming". Enjoy reading!
  Version: 03/11/2010. Thanks Louis Mandel, Tayeb Bouhadiba and Peng Li for their comments.

Conferences where I was:

• VMCAI 2010, RAIM 2009, ICESS 2009, NSV-II, SLA++P'08, POPL'08, VMCAI'08, 30Y of AI, AFADL'07, PLDI'06, LCTES'06, ETAPS'06

---

Thanks Hugo Gimbert for this web page style.