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 metadatas

Cited literature [22 references]  Display  Hide  Download

https://hal.inria.fr/hal-01111588
Contributor : Alan Schmitt <>
Submitted on : Thursday, February 12, 2015 - 5:01:30 PM
Last modification on : Wednesday, February 20, 2019 - 2:32:01 PM
Long-term archiving on : Sunday, April 16, 2017 - 8:06:14 AM

File

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

Identifiers

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. ⟨10.1145/2676724.2693174⟩. ⟨hal-01111588⟩

Share

Metrics

Record views

3501

Files downloads

413