A formally-verified alias analysis

Abstract : This paper reports on the formalization and proof of soundness, using the Coq proof assistant, of an alias analysis: a static analysis that approximates the flow of pointer values. The alias analysis considered is of the points-to kind and is intraprocedural, flow-sensitive, field-sensitive, and untyped. Its soundness proof follows the general style of abstract interpretation. The analysis is designed to fit in the CompCert C verified compiler, supporting future aggressive optimizations over memory accesses.
Type de document :
Communication dans un congrès
Hawblitzel, Chris and Miller, Dale. CPP 2012 - Second International Conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. Springer, 7679, pp.11-26, 2012, Lecture Notes in Computer Science; Certified Programs and Proofs. <10.1007/978-3-642-35308-6_5>
Liste complète des métadonnées


https://hal.inria.fr/hal-00773109
Contributeur : Xavier Leroy <>
Soumis le : vendredi 11 janvier 2013 - 15:59:42
Dernière modification le : lundi 14 janvier 2013 - 10:34:10
Document(s) archivé(s) le : samedi 1 avril 2017 - 04:00:28

Fichier

alias-analysis.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

Citation

Valentin Robert, Xavier Leroy. A formally-verified alias analysis. Hawblitzel, Chris and Miller, Dale. CPP 2012 - Second International Conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. Springer, 7679, pp.11-26, 2012, Lecture Notes in Computer Science; Certified Programs and Proofs. <10.1007/978-3-642-35308-6_5>. <hal-00773109>

Partager

Métriques

Consultations de
la notice

160

Téléchargements du document

86