Difference between revisions of "VPL"
Jump to navigation
Jump to search
(add VSTTE) |
|||
| 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== | ||
| Line 19: | Line 15: | ||
* [[: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]] | * [[:File:VPL 2014-03-19.zip|2014-03-19]] | ||
| + | * [http://www-verimag.imag.fr/~boulme/vstte2014.tgz 2014-04-30] | ||
Revision as of 15:56, 27 June 2014
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
