Title
Verification of Program Transformations with Inductive Refinement Types
Abstract
AbstractHigh-level transformation languages like Rascal include expressive features for manipulating large abstract syntax trees: first-class traversals, expressive pattern matching, backtracking, and generalized iterators. We present the design and implementation of an abstract interpretation tool, Rabit, for verifying inductive type and shape properties for transformations written in such languages. We describe how to perform abstract interpretation based on operational semantics, specifically focusing on the challenges arising when analyzing the expressive traversals and pattern matching. Finally, we evaluate Rabit on a series of transformations (normalization, desugaring, refactoring, code generators, type inference, etc.) showing that we can effectively verify stated properties.
Year
DOI
Venue
2021
10.1145/3409805
ACM Transactions on Software Engineering and Methodology
Keywords
DocType
Volume
Transformation languages, abstract interpretation, static analysis
Journal
30
Issue
ISSN
Citations 
1
1049-331X
0
PageRank 
References 
Authors
0.34
0
4
Name
Order
Citations
PageRank
Ahmad Salim Al-Sibahi1273.10
Thomas P. Jensen200.34
Aleksandar S. Dimovski3598.60
Andrzej Wasowski4128260.47