Deriving Abstract Interpreters from Skeletal Semantics
Programming Languages
2023-09-15 v1
Abstract
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.
Cite
@article{arxiv.2309.07298,
title = {Deriving Abstract Interpreters from Skeletal Semantics},
author = {Thomas Jensen and Vincent Rébiscoul and Alan Schmitt},
journal= {arXiv preprint arXiv:2309.07298},
year = {2023}
}
Comments
In Proceedings EXPRESS/SOS2023, arXiv:2309.05788