Difference between revisions of "VPL"
Jump to navigation
Jump to search
(Created page with "'''VPL''' is the {Verasco|VERIMAG} Polyhedra Library. It consists in : * An Objective Caml library, implementing polyhedral operations. * A Coq checker and wrappers, which p...") |
|||
| Line 4: | Line 4: | ||
* An Objective Caml library, implementing polyhedral operations. | * An Objective Caml library, implementing polyhedral operations. | ||
* A Coq checker and wrappers, which provably check the correctness (at least in one direction) of the polyhedral operations. | * A Coq checker and wrappers, which provably check the correctness (at least in one direction) of the polyhedral operations. | ||
| + | |||
| + | ==Prerequisites== | ||
| + | * A recent version of OCaml with ocamlfind (findlib) and the [http://forge.ocamlcore.org/projects/zarith ZArith] library | ||
| + | * If using the Coq development: Coq 8.4pl1 | ||
==Distribution== | ==Distribution== | ||
===OCaml library=== | ===OCaml library=== | ||
| + | As a convenience, we distribute the OCaml library standalone, without any dependency on Coq developments. | ||
| + | |||
* [http://verasco.imag.fr/wiki/File:Vpl_caml_2013-05-16.zip 2013-05-16] | * [http://verasco.imag.fr/wiki/File:Vpl_caml_2013-05-16.zip 2013-05-16] | ||
Revision as of 13:08, 17 May 2013
VPL is the {Verasco|VERIMAG} Polyhedra Library.
It consists in :
- An Objective Caml library, implementing polyhedral operations.
- A Coq checker and wrappers, which provably check the correctness (at least in one direction) of the polyhedral operations.
Prerequisites
- A recent version of OCaml with ocamlfind (findlib) and the ZArith library
- If using the Coq development: Coq 8.4pl1
Distribution
OCaml library
As a convenience, we distribute the OCaml library standalone, without any dependency on Coq developments.
