An Abstract Memory Functor for Verified C Static Analyzers

Sandrine Blazy 1 Vincent Laporte 2 David Pichardie 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : Abstract interpretation provides advanced techniques to infer numerical invariants on programs. There is an abundant literature about numerical abstract domains that operate on scalar variables. This work deals with lifting these techniques to a realistic C memory model. We present an abstract memory functor that takes as argument any standard numerical abstract domain, and builds a memory abstract domain that finely tracks properties about memory contents, taking into account union types, pointer arithmetic and type casts. This functor is implemented and verified inside the Coq proof assistant with respect to the CompCert compiler memory model. Using the Coq extraction mechanism, it is fully executable and used by the Verasco C static analyzer.
Type de document :
Communication dans un congrès
ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Sep 2016, Nara, Japan. ACM, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), pp.14, 2016, 〈http://conf.researchr.org/home/icfp-2016/〉. 〈10.1145/2951913.2951937〉
Liste complète des métadonnées

Littérature citée [23 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/hal-01339969
Contributeur : Sandrine Blazy <>
Soumis le : mardi 25 octobre 2016 - 11:45:25
Dernière modification le : mercredi 16 mai 2018 - 11:23:28
Document(s) archivé(s) le : vendredi 3 février 2017 - 12:17:32

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Licence


Distributed under a Creative Commons Paternité - Pas d'utilisation commerciale - Pas de modification 4.0 International License

Identifiants

Citation

Sandrine Blazy, Vincent Laporte, David Pichardie. An Abstract Memory Functor for Verified C Static Analyzers. ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), Sep 2016, Nara, Japan. ACM, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming (ICFP 2016), pp.14, 2016, 〈http://conf.researchr.org/home/icfp-2016/〉. 〈10.1145/2951913.2951937〉. 〈hal-01339969〉

Partager

Métriques

Consultations de la notice

1050

Téléchargements de fichiers

150