Martin Bodin (ENS Lyon and Inria) |
Thomas Jensen (Inria) |
Alan Schmitt (Inria) |
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. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.129.23 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |