Difference between revisions of "VPL"
Jump to navigation
Jump to search
| 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. | ||
| + | |||
| + | It implements the constraint-only algorithms for convex polyhedra found in {{bibv|Fouilhe_et_al_SAS2013}}. | ||
==Prerequisites== | ==Prerequisites== | ||
Revision as of 13:39, 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.
It implements the constraint-only algorithms for convex polyhedra found in [Fouilhe_et_al_SAS2013].
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.
