Verification of high-level transformations with inductive refinement types

Ahmad Salim Al-Sibahi; Thomas P. Jensen; Aleksandar Dimovski; Andrzej Wasowski

doi:10.1145/3278122.3278125

Verification of high-level transformations with inductive refinement types

Ahmad Salim Al-Sibahi, Thomas P. Jensen, Aleksandar Dimovski, Andrzej Wasowski

Software Quality Research

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

Abstract

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.

Original language	English
Title of host publication	Proceedings of the 17th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, {GPCE} 2018, Boston, MA, USA, November 5-6, 2018
Number of pages	14
Publisher	Association for Computing Machinery
Publication date	2018
Pages	147-160
ISBN (Print)	978-1-4503-6045-6
DOIs	https://doi.org/10.1145/3278122.3278125
Publication status	Published - 2018

Keywords

high-level transformation languages
abstract syntax trees
abstract interpretation
operational semantics
code transformations verification

Access to Document

10.1145/3278122.3278125

2018-gpcse-asal-verification-rascalAccepted author manuscript, 844 KB

Cite this

Al-Sibahi, A. S., Jensen, T. P., Dimovski, A., & Wasowski, A. (2018). Verification of high-level transformations with inductive refinement types. In Proceedings of the 17th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, {GPCE} 2018, Boston, MA, USA, November 5-6, 2018 (pp. 147-160). Association for Computing Machinery. https://doi.org/10.1145/3278122.3278125

@inproceedings{279e33597ec347069254fa75979e438d,

title = "Verification of high-level transformations with inductive refinement types",

abstract = "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.",

keywords = "high-level transformation languages, abstract syntax trees, abstract interpretation, operational semantics, code transformations verification, high-level transformation languages, abstract syntax trees, abstract interpretation, operational semantics, code transformations verification",

author = "Al-Sibahi, {Ahmad Salim} and Jensen, {Thomas P.} and Aleksandar Dimovski and Andrzej Wasowski",

year = "2018",

doi = "10.1145/3278122.3278125",

language = "English",

isbn = "978-1-4503-6045-6",

pages = "147--160",

booktitle = "Proceedings of the 17th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, {GPCE} 2018, Boston, MA, USA, November 5-6, 2018",

publisher = "Association for Computing Machinery",

address = "United States",

}

Al-Sibahi, AS, Jensen, TP, Dimovski, A & Wasowski, A 2018, Verification of high-level transformations with inductive refinement types. in Proceedings of the 17th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, {GPCE} 2018, Boston, MA, USA, November 5-6, 2018. Association for Computing Machinery, pp. 147-160. https://doi.org/10.1145/3278122.3278125

Verification of high-level transformations with inductive refinement types. / Al-Sibahi, Ahmad Salim; Jensen, Thomas P.; Dimovski, Aleksandar et al.
Proceedings of the 17th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, {GPCE} 2018, Boston, MA, USA, November 5-6, 2018. Association for Computing Machinery, 2018. p. 147-160.

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

T1 - Verification of high-level transformations with inductive refinement types

AU - Al-Sibahi, Ahmad Salim

AU - Jensen, Thomas P.

AU - Dimovski, Aleksandar

AU - Wasowski, Andrzej

PY - 2018

Y1 - 2018

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 - high-level transformation languages

KW - abstract syntax trees

KW - abstract interpretation

KW - operational semantics

KW - code transformations verification

KW - high-level transformation languages

KW - abstract syntax trees

KW - abstract interpretation

KW - operational semantics

KW - code transformations verification

U2 - 10.1145/3278122.3278125

DO - 10.1145/3278122.3278125

M3 - Article in proceedings

SN - 978-1-4503-6045-6

SP - 147

EP - 160

BT - Proceedings of the 17th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, {GPCE} 2018, Boston, MA, USA, November 5-6, 2018

PB - Association for Computing Machinery

ER -

Al-Sibahi AS, Jensen TP, Dimovski A, Wasowski A. Verification of high-level transformations with inductive refinement types. In Proceedings of the 17th ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences, {GPCE} 2018, Boston, MA, USA, November 5-6, 2018. Association for Computing Machinery. 2018. p. 147-160 doi: 10.1145/3278122.3278125

Verification of high-level transformations with inductive refinement types

Abstract

Keywords

Access to Document

Fingerprint

Cite this