2018-00911 - Post-Doctoral Position /ProvenMPFR
Le descriptif de l’offre ci-dessous est en Anglais

Niveau de diplôme exigé : Thèse ou équivalent

Fonction : Post-Doctorant

Contexte et atouts du poste

The recruited person will work in the INRIA Nancy-Grand Est and LORIA centers (about 500 researchers), more particularly in the Caramba team (about 15 researchers).

The main working environment of the team is GNU Linux, with acces (if needed) to the Grid 5000 testbed, and to the ci.inria.fr continuous integration platform.

Mission confiée

For a better knowledge of the proposed research subject :
A state of the art, bibliography and scientific references are available at the following URL: https://mpfr.org

Collaboration :
The recruited person will work in connection with Vincent Lefevre (team AriC, Inria, Lyon)

Principales activités

The aim of this project is to formally prove the low-level routines of the GNU MPFR library, which is used --- among other software tools --- by the compiler suite GCC, the CGAL computational geometry library, the Gnome calculator, the Julia language, the computer algebra systems Maple and SageMath, the Matlab multiple-precision toolbox, the GNU Octave software tool.

When the Pentium FDIV bug was discovered in 1994, Intel hired John Harrison, a specialist of formal proof, to prove the conformance of its next-generation processors. Instead of waiting for a critical bug to be found in GNU MPFR, the long-term objective is to formally prove the correctness of the MPFR library. We want not only to formally prove the algorithms used, but also their implementation in the C language. The goal of the ProvenMPFR postdoctoral project is to investigate on the low-level MPFR routines, and determine the best tools to realize that project.

The ProvenMPFR project will explore the formal proof of algorithms computing correctly-rounded results for arbitrary-precision floating-point numbers. Instead of proving algorithms with ``pen and pencil'', the goal is to prove the concrete implementation of those algorithms in MPFR. We will mostly aim at the basic arithmetic routines (addition, subtraction, multiplication, division, square root) for precisions up to 128 bits. The goal of the ProvenMPFR project is: (1) to explore the different tools currently available, that would allow to formally prove the algorithms used by MPFR and their implementation in the C language; (2) to instrument at least two of these tools to prove the correctness of the basic MPFR routines in small precision. In particular, we should consider at least a tool doing code extraction, and a tool working with code annotation. In the case of code extraction, the extracted code should be as efficient as that currently used by the MPFR library, so that we can replace it by the extracted code. In the case of code annotation, modifying the MPFR code is allowed, as long as its efficiency remains the same. The MPFR library being evolving continuously, that comparison should also take into account how easy it will be for the MPFR developers --- who are not fluent in formal proof --- to learn and use those tools. The results of this postdoctoral position will be submitted in journals or conferences in the domain of formal proof and/or of computer arithmetic.




A PhD in computer science is required. This postdoctoral position requires some experience in the concrete application of one or more formal proof tools, with published articles in that domain. A good knowledge of the C language, beyond small programs, is required, since it will be necessary to read and understand the C code used by MPFR, and if needed modify it to make the proof easier, but without any loss of efficiency. Some knowledge of computer arithmetic (IEEE 754 standard, arbitrary precision) is welcome but not required.

Avantages sociaux

  • Subsidised catering service
  • Partially-reimbursed public transport
  • Social security
  • Paid leave
  • Flexible working hours
  • Sports facilities


Salary : 2653,00€ gross/month