Formal proofs of code generation and verification tools
Résumé
Tool-assisted verification of critical software has great potential but is limited by two risks: unsoundness of the verification tools, and miscompilation when generating executable code from the sources that were verified. A radical solution to these two risks is the deductive verification of compilers and verification tools themselves. In this invited talk, I describe two ongoing projects along this line: CompCert, a verified C~compiler, and Verasco, a verified static analyzer based on abstract interpretation.
Domaines
Langage de programmation [cs.PL]
Origine : Fichiers produits par l'(les) auteur(s)
Loading...