Verification of Program Transformations with Inductive Refinement Types
Research output: Contribution to journal › Journal article › Research › peer-review
Standard
Verification of Program Transformations with Inductive Refinement Types. / Al-Sibahi, Ahmad Salim; Jensen, Thomas P.; Dimovski, Aleksandar S.; Wasowski, Andrzej.
In: ACM Transactions on Software Engineering and Methodology, Vol. 30, No. 1, 5, 2021.Research output: Contribution to journal › Journal article › Research › peer-review
Harvard
APA
Vancouver
Author
Bibtex
}
RIS
TY - JOUR
T1 - Verification of Program Transformations with Inductive Refinement Types
AU - Al-Sibahi, Ahmad Salim
AU - Jensen, Thomas P.
AU - Dimovski, Aleksandar S.
AU - Wasowski, Andrzej
N1 - Publisher Copyright: © 2021 ACM.
PY - 2021
Y1 - 2021
N2 - High-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.
AB - High-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.
KW - abstract interpretation
KW - static analysis
KW - Transformation languages
U2 - 10.1145/3409805
DO - 10.1145/3409805
M3 - Journal article
AN - SCOPUS:85099877444
VL - 30
JO - ACM Transactions on Software Engineering and Methodology
JF - ACM Transactions on Software Engineering and Methodology
SN - 1049-331X
IS - 1
M1 - 5
ER -
ID: 285381548