VPL

VPL is the {Verasco|VERIMAG} Polyhedra Library.

It consists in :

• An Objective Caml library (called the backend), implementing polyhedral operations. It implements the constraint-only algorithms for convex polyhedra found in [Fouilhe_et_al_SAS2013].
• A Coq checker and wrappers (called the frontend), which provably check the soundness of the polyhedral operations. For Coq, the frontend offers two interface of the polyhedral domain: one formalizes (boxedCoq/) the possible (but unexpected) side effects of the backend whereas the other is pure (but implicitly assumes that the backend is also pure, and in particular ZArith). This latter interface is used in Verasco. For the former, we provide a toy demo (see boxedCoq/Demo*) using a postcondition computation based on this polyhedral abstract domain. See our VSTTE2014 paper for more explanations on these ideas.

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# version (tried under Mono).
• 2014-03-19
• 2014-04-30