Deriving Abstract Interpreters from Skeletal Semantics
Thomas Jensen (INRIA), Vincent R\'ebiscoul (Universite de Rennes),, Alan Schmitt (INRIA)
TL;DR
This paper presents a methodology to automatically derive executable abstract interpreters from formal language semantics using Skeletal Semantics, enabling correctness guarantees through compositionality.
Contribution
It introduces a novel approach to generate abstract interpreters from skeletal semantics, ensuring correctness via compositional reasoning.
Findings
Successfully derived a Value Analysis for a small imperative language
Demonstrated the generic applicability of the method
Ensured correctness through compositionality
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.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.