VPL: Verimag Polyhedra Library (Verified Polyhedra Library). The VPL is an Ocaml library allowing to compute with convex polyhedra. It provides standard operators -- certified in Coq -- to use this library as an abstract domain of polyhedra.