Sites Inria

Version française

See all appointments

© INRIA Sophie Auvin - G comme Grille

Research teams seminar

Gallium seminar


In the formal-methods world, the hardware industry's use of formal verification is often touted as quite advanced compared to the state of practice in software.  The claim seems to be true, but software-verification specialists might be surprised at how weak are the theorems that tend to be proved about hardware.  

In this talk, I will present our Kami framework for the Coq proof assistant, which applies to digital-hardware verification the sorts of functional-correctness techniques that are well-known in the programming-languages community, with some twists.

Place : Inria de Paris- 2 rue Simone Iff - Salle Lions 1- bâtiment C

Guest(s) : Adam Chlipala


lire la suite