Difference between revisions of "VPL"
Jump to navigation
Jump to search
(add VSTTE) |
(Github link) |
||
| Line 10: | Line 10: | ||
* GNU Make | * GNU Make | ||
| − | ==Distribution== | + | ==Recent versions== |
| + | Recent work is on [https://github.com/VERIMAG-Polyhedra/VPL GitHub] | ||
| + | |||
| + | ==Old Distribution== | ||
===OCaml library=== | ===OCaml library=== | ||
As a convenience, we distribute the OCaml library standalone, without any dependency on Coq developments. | As a convenience, we distribute the OCaml library standalone, without any dependency on Coq developments. | ||
Latest revision as of 17:06, 8 February 2017
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
Recent versions
Recent work is on GitHub
Old 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
