Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version)
Programming Languages
2013-09-23 v1 Logic in Computer Science
Abstract
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.
Cite
@article{arxiv.1309.5149,
title = {Pretty-big-step-semantics-based Certified Abstract Interpretation (Preliminary version)},
author = {Martin Bodin and Thomas Jensen and Alan Schmitt},
journal= {arXiv preprint arXiv:1309.5149},
year = {2013}
}
Comments
In Proceedings Festschrift for Dave Schmidt, arXiv:1309.4557