Formal verification of compilers and static analyzers.

Sandrine Blazy 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Static analysis – the automatic determination of simple properties of a program – is the basis both for optimizing compilation and for verification of safety properties such as absence of run-time errors. To support the use of static analyses in verified compilers and in high-confidence verification environments, the analyses must be proved to be sound. In this invited talk, I will review some ongoing work in this direction in the CompCert and Verasco projects, in particular the construction and formal verification of a modular static analyzer based on abstract interpretation.
Type de document :
Communication dans un congrès
PLMW@POPL 2015 - Programming Languages Mentoring Workshop, Jan 2015, Mumbai, India
Liste complète des métadonnées

https://hal.inria.fr/hal-01242094
Contributeur : Sandrine Blazy <>
Soumis le : vendredi 11 décembre 2015 - 14:25:21
Dernière modification le : mardi 16 janvier 2018 - 15:54:17

Identifiants

  • HAL Id : hal-01242094, version 1

Citation

Sandrine Blazy. Formal verification of compilers and static analyzers. . PLMW@POPL 2015 - Programming Languages Mentoring Workshop, Jan 2015, Mumbai, India. 〈hal-01242094〉

Partager

Métriques

Consultations de la notice

242