Introduction to POLKA

New Polka is a library to handle convex polyhedra, whose constraints and generators have rational coefficients. It is programmed in ANSI C, so you can use it in any C or C++ programs. An interface to the language OCaml version 3.00 is also provided. This library is currently used in my verification tool NBac, and also by others research teams working on static analysis and abstract interpretation.

It is mainly based on the IRISA library Polylib and the old library used in the Polka tool inside the synchronous team of the laboratory VERIMAG. The main motivation to develop a new library was the need for multi-precision integers and 64 bits integers. The interface and memory management have also been improved (according to the author !), and saturation matrices can be kept in memory, thus saving computation time. There is also an option to handle strict constraints like x>y.

Implemented operations include creation of polyhedra from constraints or generators, intersection, convex hull, image and preimage by linear transformations, widening operator (as used in linear relation analysis, see publications of Nicolas Halbwachs about this technique), and inspection of saturation matrices.

The C interface is simple but also quite rough. The OCaml interface offers however pretty input and output of constraints, matrices and polyhedra, and gives you a polyhedra desk calculator thanks to the OCaml toplevel.