Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

Cited literature [22 references]  Display  Hide  Download
Contributor : Alan Schmitt Connect in order to contact the contributor
Submitted on : Thursday, February 12, 2015 - 5:01:30 PM
Last modification on : Thursday, January 20, 2022 - 5:33:31 PM
Long-term archiving on: : Sunday, April 16, 2017 - 8:06:14 AM


BodinJensenSchmitt-CPP 2015-Ce...
Files produced by the author(s)



Martin Bodin, Thomas Jensen, Alan Schmitt. Certified Abstract Interpretation with Pretty-Big-Step Semantics. Certified Programs and Proofs (CPP 2015), Jan 2015, Mumbai, India. ⟨10.1145/2676724.2693174⟩. ⟨hal-01111588⟩



Les métriques sont temporairement indisponibles