  Polyhedra form an established abstract domain for inferring runtime
properties of programs using abstract interpretation. Computations on them need
to be certified for the whole static analysis results to be trusted. In this
work, we look at how far we can get down the road of a posteriori verification
to lower the overhead of certification of the abstract domain of polyhedra. We
demonstrate methods for making the cost of inclusion certificate generation
negligible. From a performance point of view, our single-representation,
constraints-based implementation compares with state-of-the-art
implementations.
