Home > Topics > Formal Proofs > Tools > Tools
Tools
- VPL (Verimag/Verified Polyhedron Library)
An abstract domain of convex polyhedra, formally verified in Coq for formally verified static analyzers, such as Verasco.
- SatAns-Cert
An OCaml wrapper certified in Coq to check answers of 2018 state-of-the-art SAT-solvers.
- The Impure Library
A Coq library to embed untrusted imperative OCaml computations (through Coq extraction toward OCaml)
- the KVX CompCert Compiler
A version of the CompCert certified compiler with instruction scheduling for pipelined processors and in particular for Kalray VLIW core (with explicit instruction parallelism at the assembly level).
- The VPL Tactic
A tactic for simplifying linear arithmetic within Coq goals, with oracles from the VPL library.
