Difference between revisions of "VPL"
Jump to navigation
Jump to search
(+F#) |
(Github link) |
||
| (4 intermediate revisions by 2 users not shown) | |||
| Line 2: | Line 2: | ||
It consists in : | It consists in : | ||
| − | * An Objective Caml library, implementing polyhedral operations. | + | * An Objective Caml library (called the backend), implementing polyhedral operations. It implements the constraint-only algorithms for convex polyhedra found in {{bibv|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 [http://forge.ocamlcore.org/projects/zarith 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 [http://hal.archives-ouvertes.fr/hal-00991853 VSTTE2014] paper for more explanations on these ideas. | |
| − | |||
| − | It implements the constraint-only algorithms for convex polyhedra found in {{bibv|Fouilhe_et_al_SAS2013}}. | ||
| − | |||
| − | |||
==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. | + | * If using the Coq development: Coq 8.4 |
| + | * GNU Make | ||
| + | |||
| + | ==Recent versions== | ||
| + | Recent work is on [https://github.com/VERIMAG-Polyhedra/VPL GitHub] | ||
| − | ==Distribution== | + | ==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. | ||
* [[: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 Coq, OCaml and F# | + | * [[:File:VPL_2013-07-09.zip|2013-07-09]] includes Coq, OCaml and F# version (tried under Mono). |
| + | * [[:File:VPL 2014-03-19.zip|2014-03-19]] | ||
| + | * [http://www-verimag.imag.fr/~boulme/vstte2014.tgz 2014-04-30] | ||
Latest revision as of 16: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
