Computing over convex polyhedra using VPL
le 13 novembre 2018
15h30 - 17h30
ENS Rennes, Salle du conseil
Plan d'accès
Intervention de David Monniaux, DR CNRS, équipe Verimag (IMAG, Grenoble), dans le cadre des séminaires du département Informatique et télécommunications.
Biographie
L'objectif pratique de ma recherche est de prouver la correction des logiciels. Ceci est relié à la théorie de la calculabilité, puisque la correction des logiciels, en général, est un problème indécidable, à la théorie de la complexité, puisque de nombreux problèmes de vérification sont de haute complexité, à la logique mathématique, et à des champs aussi divers que la théorie des jeux, l'algèbre, et l'optimisation convexe.
Je me suis notamment intéressé à prouver des propriétés de logiciels critiques utilisés en aviation civile (notamment par rapport aux dépassements de capacité arithmétique et des calculs en virgule flottante). J'ai également travaillé sur les protocoles cryptographiques et les systèmes probabilistes.
In contrast, with a constraint-only representation, it is possible to provide, along with each constraint of the result polyhedron, a certificate of its soundness. This is sufficient to certify that the computed result contains the ideal result, which is enough to certify that many program analyses are correct.
In this talk I will discuss:
- The “conventional” constraint-only algorithms based on Fourier-Motzkin elimination.
- Our newer approach based on parametric linear programming.
- How to obtain trustable, exact results from parallel efficient code implemented using floating-point arithmetic and untrusted solvers.
- Other applications of parametric linear programming.
- Thématique(s)
- Formation, Recherche - Valorisation
- Contact
- Luc Bougé
Mise à jour le 5 décembre 2018