Certified Abstract Interpretation with Pretty-Big-Step Semantics

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 : This paper describes an investigation into developing certified abstract interpreters from big-step semantics using the Coq proof assistant. We base our approach on Schmidt’s abstract interpretation principles for natural semantics, and use a pretty-big-step (PBS) semantics, a semantic format proposed by Charguéraud. We propose a systematic representation of the PBS format and implement it in Coq. We then show how the semantic rules can be abstracted in a methodical fashion, independently of the chosen abstract domain, to produce a set of abstract inference rules that specify an abstract interpreter. We prove the correctness of the abstract interpreter in Coq once and for all, under the assumption that abstract operations faithfully respect the concrete ones. We finally show how to define correct-by-construction analyses: their correction amounts to proving they belong to the abstract semantics.
Type de document :
Communication dans un congrès
Certified Programs and Proofs (CPP 2015), Jan 2015, Mumbai, India. Proceedings of the 2015 Conference on Certified Programs and Proofs. <10.1145/2676724.2693174>
Liste complète des métadonnées


https://hal.inria.fr/hal-01111588
Contributeur : Alan Schmitt <>
Soumis le : jeudi 12 février 2015 - 17:01:30
Dernière modification le : vendredi 17 février 2017 - 16:11:11
Document(s) archivé(s) le : dimanche 16 avril 2017 - 08:06:14

Fichier

BodinJensenSchmitt-CPP 2015-Ce...
Fichiers produits par l'(les) auteur(s)

Identifiants

Citation

Martin Bodin, Thomas Jensen, Alan Schmitt. Certified Abstract Interpretation with Pretty-Big-Step Semantics. Certified Programs and Proofs (CPP 2015), Jan 2015, Mumbai, India. Proceedings of the 2015 Conference on Certified Programs and Proofs. <10.1145/2676724.2693174>. <hal-01111588>

Partager

Métriques

Consultations de
la notice

1285

Téléchargements du document

223