Certified Abstract Interpretation with Pretty-Big-Step Semantics

International audienceThis paper describes an investigation into developing certified abstractinterpreters from big-step semantics using the Coq proof assistant.We base our approach on Schmidt’s abstract interpretationprinciples for natural semantics, and use a pretty-big-step (PBS) semantics,a semantic format proposed by Charguéraud. We proposea systematic representation of the PBS format and implement it inCoq. We then show how the semantic rules can be abstracted in amethodical fashion, independently of the chosen abstract domain,to produce a set of abstract inference rules that specify an abstractinterpreter. We prove the correctness of the abstract interpreter inCoq once and for all, under the assumption that abstract operationsfaithfully respect the concrete ones. We finally show how to definecorrect-by-construction analyses: their correction amounts to provingthey belong to the abstract semantics