Thomas Jensen (INRIA) |
Vincent Rébiscoul (Universite de Rennes) |
Alan Schmitt (INRIA) |
This paper describes a methodology for defining an executable abstract interpreter from a formal description of the semantics of a programming language. Our approach is based on Skeletal Semantics and an abstract interpretation of its semantic meta-language. The correctness of the derived abstract interpretation can be established by compositionality provided that correctness properties of the core language-specific constructs are established. We illustrate the genericness of our method by defining a Value Analysis for a small imperative language based on its skeletal semantics. |
ArXived at: https://dx.doi.org/10.4204/EPTCS.387.8 | bibtex | |
Comments and questions to: eptcs@eptcs.org |
For website issues: webmaster@eptcs.org |