Certified Certification Tools

Point of contact

Virgile Prevosto, CEA List


Formal software verification tools are themselves programs, hence can contain bugs. Therefore,they should themselves be verified as much as possible, to minimize the Trusted Computing Base of the system. Efforts in this direction include in particular:

  • The formalization of the semantics of existing programming languages (e.g. C) within proof assistants such as Coq
  • The development of certified implementation of software analyzers
  • Generating proof certificates from automated theorem provers, that can be independently checked

A few references

Related master programs