Partager cette page :

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.

Séminaire Informatique et télécommunications

Séminaire 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. 

Abstract
 
Convex polyhedra occur in a variety of mathematical and computer science contexts, including static program analysis and some advanced compilation schemes. The usual approach to computing over them is the “dual description”, both as the convex hull of a set of generators (vertices, for bounded polyhedra) and as the solution of a system of linear equalities and inequalities (the constraints). 
 
This approach has many advantages but suffers from two drawbacks: the generator representation is exponential in the dimension in some common cases in program analysis (thus users tended to drastically limit the dimension), and it is difficult to check the final result without somehow checking the correctness of the full algorithm of conversion between descriptions.

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.
You are welcome to download our library VPL: https://github.com/VERIMAG-Polyhedra/VPL

Thématique(s)
Formation, Recherche - Valorisation
Contact
Luc Bougé

Mise à jour le 5 décembre 2018