Auditorium (IMAG)
11 décembre 2017 - 14h00
New Algorithmics for Polyhedral Calculus via Parametric Linear Programming (Phd Defense)
par Alexandre Maréchal de Verimag
Abstract: 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 Coq 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 Coq tactic for learning equalities in linear arithmetic.
