Difference between revisions of "VPL"
Jump to navigation
Jump to search
| Line 11: | Line 11: | ||
==Prerequisites== | ==Prerequisites== | ||
* A recent version of OCaml with ocamlfind (findlib) and the [http://forge.ocamlcore.org/projects/zarith ZArith] library | * 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. | + | * If using the Coq development: Coq 8.4 |
| + | * GNU Make | ||
==Distribution== | ==Distribution== | ||
Revision as of 15:33, 27 June 2014
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.
It implements the constraint-only algorithms for convex polyhedra found in [Fouilhe_et_al_SAS2013].
The library (if extracted using an experimental version of Coq; we supply the extracted files) can also be compiled under F# (tried under Mono).
Prerequisites
- A recent version of OCaml with ocamlfind (findlib) and the ZArith library
- If using the Coq development: Coq 8.4
- GNU Make
Distribution
OCaml library
As a convenience, we distribute the OCaml library standalone, without any dependency on Coq developments.
- 2013-05-16
- 2013-07-09 includes Coq, OCaml and F# versions
- 2014-03-19
