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.
Connections
Explore this paper’s authors, topics and related work.
Building this map preview
BZPEER is loading the nearby papers, people, topics and institutions for this page.
Reviews 0
Write a review
No reviews yet.
Discussion 0
Add a comment
No comments yet.