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 metadatas

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/hal-00927400
Contributor : Alan Schmitt <>
Submitted on : Monday, January 13, 2014 - 9:29:57 AM
Last modification on : Wednesday, February 20, 2019 - 2:32:01 PM
Long-term archiving on : Sunday, April 13, 2014 - 10:21:36 PM

File

essay.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-00927400, version 1

Citation

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⟩

Share

Metrics

Record views

3631

Files downloads

336