I am currently in post-doc position in informatics at LSL in the center CEA-Saclay. My current area of interest is the verification and certification of floating-point C programs by formal methods. Specifically, I am working on the value analysis of floating-point C programs by abstract interpretation in the Frama-C platform, a tool for formal verification of C code, with industrial applications in order to ensure the correctness of critical softwares. Frama-C is constructed by a set of plugins dedicated to specific tasks. For example, Jessie is the plugin for deductive verifications of programs by Hoare logic and weakest precondition computations, the plugin ValViewer for the value analysis of variables in C programs by abstract interpretation.

For a detailed presentation of my research project click here (in French).

Areas of research specialization

  • Floating-point arithmetic
  • Formal methods for static analysis of programs
  • Deductive verification of floating-point C programs
  • Value analysis of C programs by abstract interpretation
  • Symbolic algebraic computation
  • Design and complexity analysis of algorithms
  • Real algebraic geometry and solving of polynomial systems
  • Nonlinear differential equations

Deductive verification of floating-point C programs

My topic of interest during my stay at the LRI of the university Paris 11 was the formal verification of the fiability of softwares. Embedded software are increasingly present in our environment, and often fulfill critical functions: nuclear energy, automotive, rail, aviation, satellites and robots. It is crucial to provide tools to ensure their proper functioning. The platform Why developed within the project-team ProVal of Inria, is a static analyser tool for C programs (Caduceus) and Java (Krakatoa) in Hoare Logic. Why generates Proof Obligations (POs) from an annotated program, they describe the variables of the program in a given point. Generated POs should be verified by automatic provers (Simplify, Ergo, Yices, CVC Lite, CVC3, haRVey, Zenon) or interactive provers (Coq, PVS, Isabelle/HOL, HOL 4, HOL-Light, Mizar) to validate the program.

My work was focused on floating-point aspects in Why. Formal methods are used to ensure the correctness of programs dealing with floating-point computations. I developed two floating-point formal models:

The first model is the Defensive model, which is an improvement of the model presented in the article "Formal Verification of Floating-Point Programs" by S. Boldo and J-C Filliâtre. This model verifies that there is no overflow in the execution of floating-point operations. Proof obligations are generated by Why to prove that there is no overflow in floating-point arithmetic.

The second model is called the Full model. This model extends the Defensive model and allows overflows in programs as special exceptions. Infinities, NaN (Not-a-Number) and signed zeros are considered as special values as in the IEEE-754 standard. Special predicates are defined to indicate the class of floating-point variables as is_finite(x), is_infinity(x), is_NaN(x), etc ...

Both models are detailed in the INRIA report 6927. They are also described in our two new articles Behavioral Properties of Floating-Point Programs and Deductive verification of floating-point programs in Frama-C.

Scientifical stays
  • Participation to Arith19 (The 19th IEEE Symposium on Computer Arithmetic), Portland, Oregon, USA, June 8-10, 2009.
  • Two weeks of research stay at the Max Planck Institute for Mathematics at Bonn in Germany, january 2006. Stay funded by the DAAD (German academic exchange service).

  • Two months of research stay at the university of Paderborn in Germany in the research group of Professor Peter Burgisser Algebraic Complexity and Algorithmic Algebra. Participation to the seminaries and discussions with the members of this group during the stay. Subjects studied : Absolute factorization of parametric multivariate polynomials and the complexity theory. May-June 2005. Stay funded by the DAAD.