2019-01430 - Post-Doctoral Research Visit F/M ProvenMPFR [S]

Contract type : Public service fixed-term contract

Level of qualifications required : PhD or equivalent

Fonction : Post-Doctoral Research Visit

Context

Team

Caramba, INRIA Nancy Grand-Est, caramba.loria.fr

 

Contacts

Paul Zimmermann (paul.zimmermann@inria.fr).

This PhD position is funded by the INRIA PRE (Projet de Recherche Exploratoire) ProvenMPFR.

 

Assignment

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.

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.

Main activities

Main activities:

  • Experiment with different formal proof frameworks
  • Instrument at least two of these tools on the GNU MPFR library (one with extraction, one without)
  • If needed, modify the GNU MPFR library to make formal proofs easier (without loss of efficiency)
  • Write formal proofs of the GNU MPFR algorithms and code
  • Write documentation and articles about the work done
  • Interact with the other MPFR developers

Skills

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

Benefits package

  • Subsidized meals
  • Partial reimbursement of public transport costs
  • Leave: 7 weeks of annual leave + 10 extra days off due to RTT (statutory reduction in working hours) + possibility of exceptional leave (sick children, moving home, etc.)
  • Possibility of teleworking (after 6 months of employment) and flexible organization of working hours
  • Professional equipment available (videoconferencing, loan of computer equipment, etc.)
  • Social, cultural and sports events and activities
  • Access to vocational training
  • Social security coverage