analyzer icon indicating copy to clipboard operation
analyzer copied to clipboard
verified publisher icon goblint

Verified Polyhedra Library support

Open sim642 opened this issue 1 year ago • 0 comments

Verified Polyhedra Library is an OCaml library for polyhedra which has been extracted from a verified Coq implementation:

  • Paper: https://hal.science/hal-02100006
  • OCaml library: https://github.com/VERIMAG-Polyhedra/VPL

Mopsa has experimented with it for js_of_ocaml because, unlike Apron, VPL is pure OCaml without any C stubs.

The downside is that it doesn't have Apron-compatible interface, so relation analysis would finally have to be decoupled from Apron's Var and Environment properly.

sim642 avatar Jul 19 '24 09:07 sim642