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.


The whole Verimag Tools page


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

info visites 3899836