Certified Abstract Interpretation with Pretty-Big-Step SemanticsReportar como inadecuado

Certified Abstract Interpretation with Pretty-Big-Step Semantics - Descarga este documento en PDF. Documentación en PDF para descargar gratis. Disponible también para leer online.

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 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.

Keywords : Verification Semantics Formal proof

Autor: Martin Bodin - Thomas Jensen - Alan Schmitt -

Fuente: https://hal.archives-ouvertes.fr/


Documentos relacionados