Difference between revisions of "VPL"

From VERASCO
Jump to navigation Jump to search
Line 16: Line 16:
  
 
* [[:File:Vpl_caml_2013-05-16.zip|2013-05-16]]
 
* [[:File:Vpl_caml_2013-05-16.zip|2013-05-16]]
* [[:File:VPL_2013-07-09.zip|2013-07-09]] includes F# version
+
* [[:File:VPL_2013-07-09.zip|2013-07-09]] includes Coq, OCaml and F# versions

Revision as of 21:18, 9 July 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.