This source archive is the release of Verimag Polyhedra Library
described in http://www-verimag.imag.fr/~boulme/vpl201503/
by Sylvain Boulmé and Alexandre Maréchal.

It contains:
 - the Ocaml backend of polyhedra operations lib/ of Alexis Fouihlé
 - the Ocaml backend of linearization lin/
 - the Coq certification coq/ (also based on files initially developed by Alexis).

In order to try a few tests, simply go in directory "coq/", and run
"make check".  This should run tests from file DemoPLTests.v (using
our certified toy analyzer of DemoPLVerifier.v)

The build system requires GNU make and version 8.4 of the Coq proof
assistant.  It also relies on the necessary tools being available in
the PATH: ocamlc, ocamlopt, ocamldep, ocamldoc, ocamlfind, coqc,
coqdep.  The backend depends on the ZArith front-end to the GMP
library and the Makefile relies on ocamlfind being configured so as to
find it.

The contents of this source archived is licensed under the 2-clause BSD
license (see file LICENSE).

Feel free to get in touch with us if you are interested in this work.
