VPL (Verified Polyhedra Library)

GENERAL INFORMATIONS

The VPL is an Ocaml library allowing to compute with convex polyhedra. It provides standard operators -- certified in Coq -- to use this library as an abstract domain of polyhedra.

Contributors: Alexis Fouilhé, Alexandre Maréchal, Sylvain Boulmé, Hang Yu, Michaël Périn, David Monniaux. Developed at Verimag and supported by ANR Verasco and ERC Stator.

If you find a bug or have any comment, feel free to contact us at verimag-polyhedra-developers@univ-grenoble-alpes.fr

INSTALLATION

1. From opam

   First, add the following repository in your opam system:

    opam repo add vpl https://raw.githubusercontent.com/VERIMAG-Polyhedra/opam-vpl/master
   

   Then, install the following packages (depending on your needs):

   • vpl-core: the ocaml library

     opam install vpl-core
     

   • coq-vpl: the Coq library (only needed to get Coq proofs about VPL operators)

     opam install coq-vpl
     

   • coq-vpltactic: the VplTactic plugin for Coq (also install coq-vpl and vpl-core)

     opam install coq-vpltactic
     

2. From sources

   1. Dependencies

      The VPL requires the following packages:

      • ocaml required version >= 4.08.0

      • zarith available in OPAM tested with version 1.4.1 and 1.9.1

      • dune available in OPAM required version >= 2.1

   2. Compiling the VPL

      (Optional) To re-extract from the coq files, simply run at the root directory

       make coq_extract
      

      To compile the VPL, simply run from the root directory

       make vpl
      

      Tests can be run by typing

       make check
      

      Finally, to install the library with ocamlfind, type

       make install
      

      To uninstall the library from ocamlfind, run

       make uninstall
      

Documentation

Documentation can be built from sources with

make doc; make open_doc

It contains the interface of main modules.

Using the VPL

There are several ways to use the library.

1. From Coq (see opam package coq-vpl)

2. As a Coq tactic (see VplTactic)

3. As an OCaml library (see opam package vpl-core)

As an OCaml library, the entry point of the VPL is the module UserInterface, which contains several version of the abstract domain. Polyhedral domains can work over Q or Z, and there are three levels of certification, which gives 6 possible domains. The level of certifications are:

• No certification: no certificate is produced. This is implemented in modules UncertifiedZ and UncertifiedQ.

• OCaml certification: Each operator of the domain produces a certificate, ie a witness of its computation that can be checked. This is implemented in modules OCamlCertifiedZ and OCamlCertifiedQ.

3. As an OCaml library (see opam package vpl-core)

• Coq certification: In addition to guarantees offered by OCaml certification, certificates are here extracted from Coq proven types. This is implemented in modules CoqCertifiedZ and CoqCertifiedQ.

Documentation

1. Online: link

2. From sources: make doc

The html documentation is then generated in the folder _build/_doc/_html/index.html