For internal staff only
Thomas Bourgeat, from the Verification and Computer Architecture Lab (VCA) at EPFL, will be giving a talk next Thursday as part of the 68nqrt seminar series. Anybody interested in hardware and formalization and/or security would be most welcome to come along! Thomas Bourgeat and Yann Herklotz (post-doc at EPFL in Thomas’s group) will be visiting the EPICURE team up until Friday, so do let know Delphine Demange if you would like to have chat with them on Friday.
Abstract: Verification of hardware designs is a crucial part of the hardware development cycle, as post-silicon errors can lead to significant delays and increased costs. Traditional hardware verification methods rely heavily on extensive testing and bounded model checking, both of which are computationally intensive and often incomplete. In this talk, we will present several aspects of an alternative hardware design and verification methodology raising the level of description of synthesizable microarchitectural designs. We will expand on our effort over the last few years to embed this design methodology in proof assistants. After introducing the design methodology, we will showcase a few previous and ongoing projects that outline various types of properties we have been interested in specifying and proving:proofs of functional correctness, low-level firmware code correctness, and microarchitectural isolation properties.
For more informations: 68nqrt.inria.fr or Delphine Demange, Epicure Research Team