Accueil > Axes > Formal Proofs > Outils > Outils

Outils



  • 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.


La page de tous les outils de Verimag


Contact | Plan du site | Site réalisé avec SPIP 4.2.16 + AHUNTSIC [CC License]

info visites 4190614