Keywords precision tuning; roundoff error; numerical accuracy; floating-point arithmetic; semidefinite programming; polynomial sums of squares; generalized eigenvalue problems; computer proofs.
Context Roundoff errors cannot be avoided when implementing numerical programs with finite precision. For each computation step, the roundoff error is very small but the accumulation of such errors can grow very quickly. A workaround to this issue consists of relying on other software tools to verify programs and proofs, allowing to certify the roundoff error bounds. This verification ability is especially important if one wants to explore a range of potential representations, for instance in the world of FPGAs. It becomes challenging when the program does not employ solely linear operations as non-linearities are inherent to many interesting computational problems in real-world applications.
The last decade has witnessed the emergence of polynomial optimization as a new field in which powerful positivity certificates from real algebraic geometry allowed to build an original framework to solve optimization problems with polynomial data. The key ingredient is the "moment-SOS’’ approach also known as "Lasserre hierarchy’’ [L01SOS] which has attracted a lot of attention in many areas (e.g. optimization, applied mathematics, program verification, engineering, theoretical computer science) with important potential applications.
Goals Here, we are interested in using polynomial optimization to certify computation of roundoff error bounds for programs involving either finite or infinite loops. This is complementary of previous research [MCD15Round], providing upper bounds for programs without loops. The aim of this PhD work is two-fold:
- Reformulating the roundoff error problems as infinite-dimensional optimization problems.
- Implementing a practical software package to compute bounds for these optimization problems. The resulting library could be included in the Real2Float verification framework (http://nl-certify.forge.ocamlcore.org/real2float.html).
Working Context The thesis will be co-advised by Victor Magron and David Monniaux. The PhD student will be hosted by the Verimag laboratory, near Grenoble in the French Alps. The Grenoble area, in addition to the surrounding skiable mountains, features one of Europe’s largest concentrations of academic/industrial research and development with a lot of students and a relatively-cosmopolite atmosphere. You can easily reach Lyon (1 hour), Geneva (1.5 hours), Torino (2 hours), Paris (3 hours by train) and Barcelona (6 hours).
Required Skills Motivated candidates should hold a Master’s degree and have a solid background in either computer science, optimization, control, electrical engineering or signal processing. Good programming skills are also required. The candidates are kindly asked to send an e-mail with "PhD candidate" in the title, a CV and motivation letter to victor.magron@imag.fr and david.monniaux@imag.fr. Knowledge of French is advantageous but does not constitute a per-requisite (and courses of French language will be covered by the lab).
