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 hasmany 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)