Pretty-big-step-semantics-based Certified Abstract Interpretation

Martin Bodin 1 Thomas Jensen 1 Alan Schmitt 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : We present a technique for deriving semantic program analyses from a natural semantics specification of the programming language. The technique is based on the pretty-big-step semantics approach applied to a language with simple objects called O'While. We specify a series of instrumentations of the semantics that makes explicit the flows of values in a program. This leads to a semantics-based dependency analysis, at the core, e.g., of tainting analysis in software security. The formalization is currently being done with the Coq proof assistant.
Type de document :
Communication dans un congrès
JFLA - 25ème Journées Francophones des Langages Applicatifs - 2014, Jan 2014, Fréjus, France. 2014
Liste complète des métadonnées

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

https://hal.inria.fr/hal-00927400
Contributeur : Alan Schmitt <>
Soumis le : lundi 13 janvier 2014 - 09:29:57
Dernière modification le : mercredi 11 avril 2018 - 02:01:09
Document(s) archivé(s) le : dimanche 13 avril 2014 - 22:21:36

Fichier

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

Identifiants

  • HAL Id : hal-00927400, version 1

Citation

Martin Bodin, Thomas Jensen, Alan Schmitt. Pretty-big-step-semantics-based Certified Abstract Interpretation. JFLA - 25ème Journées Francophones des Langages Applicatifs - 2014, Jan 2014, Fréjus, France. 2014. 〈hal-00927400〉

Partager

Métriques

Consultations de la notice

2388

Téléchargements de fichiers

300