Home > Topics > Formal Proofs > 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.

The whole Verimag Tools page

Contact | Site Map | Site powered by SPIP 4.2.13 + AHUNTSIC [CC License]

info visites 4000971