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 Chamois CompCert Compiler
A version of the CompCert certified compiler with added optimizations and a backend for the Kalray KVX processor.
- The Impure Library
A Coq library to embed untrusted imperative OCaml computations (through Coq extraction toward OCaml)
- The VPL Tactic
A tactic for simplifying linear arithmetic within Coq goals, with oracles from the VPL library.
