Verification of Program Transformations with Inductive Refinement Types

Autor: Aleksandar S. Dimovski, Andrzej Wąsowski, Thomas Jensen, Ahmad Salim Al-Sibahi
Přispěvatelé: University of Copenhagen = Københavns Universitet (KU), Software certification with semantic analysis (CELTIQUE), Inria Rennes – Bretagne Atlantique, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-LANGAGE ET GÉNIE LOGICIEL (IRISA-D4), Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National de Recherche en Informatique et en Automatique (Inria)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Université de Rennes (UNIV-RENNES)-CentraleSupélec-IMT Atlantique Bretagne-Pays de la Loire (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Bretagne Sud (UBS)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Institut de Recherche en Informatique et Systèmes Aléatoires (IRISA), Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-Institut National des Sciences Appliquées (INSA)-Université de Rennes (UNIV-RENNES)-École normale supérieure - Rennes (ENS Rennes)-Centre National de la Recherche Scientifique (CNRS)-Université de Rennes 1 (UR1), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT), IT University of Copenhagen, University of Copenhagen = Københavns Universitet (UCPH), Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), Institut Mines-Télécom [Paris] (IMT)-Institut Mines-Télécom [Paris] (IMT)-Université de Rennes (UR)-Institut National des Sciences Appliquées - Rennes (INSA Rennes), Institut National des Sciences Appliquées (INSA)-Institut National des Sciences Appliquées (INSA)-Université de Bretagne Sud (UBS)-École normale supérieure - Rennes (ENS Rennes)-CentraleSupélec-Centre National de la Recherche Scientifique (CNRS)-IMT Atlantique (IMT Atlantique), IT University of Copenhagen (ITU)
Jazyk: angličtina
Rok vydání: 2021
Předmět:
Program schemes
Computer science
• Software and its engineering → Translator writing systems and compiler generators
02 engineering and technology
computer.software_genre
Operational semantics
CCS Concepts: • Theory of computation → Program verification
Abstract syntax
0202 electrical engineering
electronic engineering
information engineering
Pattern matching
abstract interpretation
Functional constructs
Inductive type
Transformation languages
Backtracking
Programming language
Type inference
transformation languages
Program analysis
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]
020207 software engineering
Abstract interpretation
Semantics
Code refactoring
static analysis
020201 artificial intelligence & image processing
Control primitives
Abstraction
computer
Software
Zdroj: ACM Transactions on Software Engineering and Methodology
ACM Transactions on Software Engineering and Methodology, Association for Computing Machinery, 2021, 30 (1), pp.1-33. ⟨10.1145/3409805⟩
ACM Transactions on Software Engineering and Methodology, 2021, 30 (1), pp.1-33. ⟨10.1145/3409805⟩
Al-Sibahi, A S, Jensen, T P, Dimovski, A S & Wasowski, A 2021, ' Verification of Program Transformations with Inductive Refinement Types ', ACM Transactions on Software Engineering and Methodology, vol. 30, no. 1, 5 . https://doi.org/10.1145/3409805
Al-Sibahi, A S, Jensen, T P, Dimovski, A & Wasowski, A 2021, ' Verification of Program Transformations with Inductive Refinement Types ', ACM Transactions on Software Engineering and Methodology, vol. 30, no. 1, 5, pp. 1-33 . https://doi.org/10.1145/3409805
ISSN: 1049-331X
DOI: 10.1145/3409805⟩
Popis: International audience; 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.
Databáze: OpenAIRE
Externí odkaz: