Programmation d'un interpréteur abstrait certifié en logique constructive

David Cachera 1 David Pichardie 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Résumé : Un analyseur statique permet de déduire automatiquement des propriétés d’un programme à partir de son code. La preuve de correction d'un analyseur repose sur des propriétés sémantiques, et devient difficile à assurer lorsque l’analyse met en oeuvre des techniques symboliques complexes. Nous proposons une adaptation de la théorie générale de l’analyse statique par interprétation abstraite au cadre de la logique constructive. L’implémentation de ce formalisme dans l’assistant de preuve Coq permet alors d’extraire automatiquement des analyseurs certifiés. Nous nous intéressons plus particulièrement à un langage impératif simple, et présentons en détail le calcul de point fixe par élargissement/rétrécissement et itération dirigée par la syntaxe.
Type de document :
Article dans une revue
Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2011, pp.28. 〈10.3166/tsi.30.381-408〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01112680
Contributeur : David Cachera <>
Soumis le : mardi 3 février 2015 - 14:34:19
Dernière modification le : mercredi 16 mai 2018 - 11:23:28

Identifiants

Citation

David Cachera, David Pichardie. Programmation d'un interpréteur abstrait certifié en logique constructive. Revue des Sciences et Technologies de l'Information - Série TSI : Technique et Science Informatiques, Lavoisier, 2011, pp.28. 〈10.3166/tsi.30.381-408〉. 〈hal-01112680〉

Partager

Métriques

Consultations de la notice

435