Contract type : Public service fixed-term contract
Level of qualifications required : PhD or equivalent
Fonction : Post-Doctoral Research Visit
Caramba, INRIA Nancy Grand-Est, caramba.loria.fr
Paul Zimmermann (email@example.com).
This PhD position is funded by the INRIA PRE (Projet de Recherche Exploratoire) ProvenMPFR.
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.
- 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
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
- 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
- Theme/Domain :
Algorithmics, Computer Algebra and Cryptology
Software engineering (BAP E)
- Town/city : Villers-lès-Nancy
- Inria Center : CRI Nancy - Grand Est
- Starting date : 2019-10-01
- Duration of contract : 1 year, 6 months
- Deadline to apply : 2019-06-05
The keys to success
Being able to work autonomously, being motivated by the formal proof of arbitrary-precision floating-point algorithms and their implementation.
How to apply
CV including a description of your research activities (2 pages max) and a short description of what you consider to be your best contributions and why (1 page max and 3 contributions max); the contributions could be theoretical or practical. Web links to the contributions should be provided. Include also a brief description of your scientific and career projects, and your scientific positioning regarding the proposed subject.
The report(s) from your PhD external reviewer(s), if applicable.
If you haven't defended yet, the list of expected members of your PhD committee (if known) and the expected date of defense (the defense, not the manuscript submission).
In addition, at least one recommendation letter from your PhD advisor should be sent directly by their author(s) to firstname.lastname@example.org.
Applications are to be sent as soon as possible.
Inria, the French national research institute for the digital sciences, promotes scientific excellence and technology transfer to maximise its impact. It employs 2,400 people. Its 200 agile project teams, generally with academic partners, involve more than 3,000 scientists in meeting the challenges of computer science and mathematics, often at the interface of other disciplines. Inria works with many companies and has assisted in the creation of over 160 startups. It strives to meet the challenges of the digital transformation of science, society and the economy.
Instruction to apply
Defence Security :
This position is likely to be situated in a restricted area (ZRR), as defined in Decree No. 2011-1425 relating to the protection of national scientific and technical potential (PPST).Authorisation to enter an area is granted by the director of the unit, following a favourable Ministerial decision, as defined in the decree of 3 July 2012 relating to the PPST. An unfavourable Ministerial decision in respect of a position situated in a ZRR would result in the cancellation of the appointment.
Recruitment Policy :
As part of its diversity policy, all Inria positions are accessible to people with disabilities.
Warning : you must enter your e-mail address in order to save your application to Inria. Applications must be submitted online on the Inria website. Processing of applications sent from other channels is not guaranteed.