Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version)

Martin Bodin
(ENS Lyon and Inria)
Thomas Jensen
Alan Schmitt

We present a technique for deriving semantic program analyses from a natural semantics specification of the programming language. The technique is based on a particular kind of semantics called pretty-big-step semantics. We present a pretty-big-step semantics of a language with simple objects called O'While and specify a series of instrumentations of the semantics that explicitates 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 has been realized with the Coq proof assistant.

In Anindya Banerjee, Olivier Danvy, Kyung-Goo Doh and John Hatcliff: Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday (Festschrift for Dave Schmidt), Manhattan, Kansas, USA, 19-20th September 2013, Electronic Proceedings in Theoretical Computer Science 129, pp. 360–383.
Published: 19th September 2013.

ArXived at: bibtex PDF
References in reconstructed bibtex, XML and HTML format (approximated).
Comments and questions to:
For website issues: