Nouvelle Algorithmique pour le Calcul Polyédral via Programmation Linéaire Paramétrique

This thesis presents the design and implementation of the Verified Polyhedra Library (VPL), a scalable library for polyhedral calculus. It provides Coq-certified polyhedral operators that work on constraints-only representation. The previous version was inefficient on crucial operations, namely variable elimination and convex hull. In this work, I present major improvements that have been made in scalability, modularity and simplicity: The certification process is generalized and simplified; polynomial guards can now be handled; computations that do not involve certification may use floating-point numbers; new algorithms are presented for minimization and detection of implicit equalities.On the one hand, the implementation of a solver for Parametric Linear Programming (PLP) problems led to improved scalability both in the dimension and in the number of constraints. Variable elimination and convex hull are now encoded as PLP. PLP is a generic tool that has many applications, and that avoids generating redundancies thanks to a normalization constraint. Additionally, we provide new operators for handling multivariate polynomials, one of which also encoded as a PLP problem.On the other hand, the certification part of the library has been greatly optimized and simplified. The VPL follows a result-verification paradigm, where complex computations are performed by untrusted oracles that generate witnesses of correctness, themselves validated by a certified C checker. Thanks to an innovative and powerful certification framework known as Polymorphic Factory Style (PFS), most cumbersome parts of the witness generation are now avoided. The flexibility of PFS is attested by the creation of a C tactic for learning equalities in linear arithmetic.Cette thèse présente la nouvelle implémentation de la Verified Polyhedra Library (VPL), une bibliothèque efficace de calcul polyédral. Elle fournit des opérateurs certifiés en Coq, s’appliquant sur des représentations en contraintes. La version précédente souffrait d’inefficacité lors d’opérateurs cruciaux, à savoir l’élimination de variables et l’enveloppe convexe. Dans ce document, je présente des améliorations importantes qui bénéficient à la modularité, la simplicité et au passage à l’échelle de la bibliothèque : le processus de certification est généralisé et simplifié ; les conditions polynomiales sont maintenant traitées ; les calculs qui n’impliquent pas de certification sont effectués en flottants ; de nouveaux algorithmes sont fournis pour la minimisation de représentation et la détection d’égalités implicites.D’un côté, l’implémentation d’un solveur de problèmes de programmation linéaire paramétrique (PLP) a mené à une meilleure efficacité tant en nombre de contraintes que de générateurs. L’élimination de variables et l’enveloppe convexe sont tous deux encodés en problème PLP.Le PLP est un outil générique possédant de nombreuses applications, et qui permet d’éviter la génération de redondances grâce à l’utilisation d’une contrainte de normalisation. De plus, nous proposons de nouveaux opérateurs pour la gestion des contraintes polynomiales, l’und’entre eux étant également encodé en tant que problème PLP.De l’autre, la certification de la bibliothèque a été grandement optimisée et simplifiée. La VPL suit un paradigme de vérification a posteriori, où les calculs non triviaux sont effectués par des oracles externes générant des témoins de correction. Ces témoins sont ensuite validéspar un vérifieur écrit en Coq. Grâce à un cadre de certification puissant et innovant, le polymorphic factory style (PFS), la plupart des aspects délicats de la génération de témoins sont maintenant évitée. La souplesse du PFS est démontrée par la création d’une tactique enCOQ qui découvre les égalités implicites en arithmétique linéaire