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.
- PADEC A Framework for Certified Self-Stabilization
PADEC is a framework to build certified proofs of self-stabilizing algorithms using the Coq proof assistant. The framework includes the definition of the computational model, lemmas for common proof patterns and case studies. A constant purpose was to convince the designers that what we formally prove using PADEC is what they expect by using definitions that are (syntactically) as close as possible to their usual definitions.
- 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.
