Skip to Main content Skip to Navigation
New interface
Conference papers

Pretty-big-step-semantics-based Certified Abstract Interpretation

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 : We present a technique for deriving semantic program analyses from a natural semantics specification of the programming language. The technique is based on the pretty-big-step semantics approach applied to a language with simple objects called O'While. We specify a series of instrumentations of the semantics that makes explicit the flows of values in a program. This leads to a semantics-based dependency analysis, at the core, e.g., of tainting analysis in software security. The formalization is currently being done with the Coq proof assistant.
Document type :
Conference papers
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Alan Schmitt Connect in order to contact the contributor
Submitted on : Monday, January 13, 2014 - 9:29:57 AM
Last modification on : Thursday, January 20, 2022 - 5:33:25 PM
Long-term archiving on: : Sunday, April 13, 2014 - 10:21:36 PM


Files produced by the author(s)


  • HAL Id : hal-00927400, version 1


Martin Bodin, Thomas Jensen, Alan Schmitt. Pretty-big-step-semantics-based Certified Abstract Interpretation. JFLA - 25ème Journées Francophones des Langages Applicatifs - 2014, Jan 2014, Fréjus, France. ⟨hal-00927400⟩



Record views


Files downloads