Difference between revisions of "VPL"

From VERASCO
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.4pl1
+
* 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.