| 1 |
Verification of Program Transformations with Inductive Refinement Types
|
|
|
|
In: ISSN: 1049-331X ; ACM Transactions on Software Engineering and Methodology ; https://hal.inria.fr/hal-03518825 ; ACM Transactions on Software Engineering and Methodology, Association for Computing Machinery, 2021, 30 (1), pp.1-33. ⟨10.1145/3409805⟩ (2021)
|
|
Abstract:
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.
|
|
Keyword:
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]; abstract interpretation; Abstraction; CCS Concepts: • Theory of computation → Program verification; Control primitives; Functional constructs; Operational semantics; Program analysis; Program schemes; Semantics; static analysis; transformation languages; • Software and its engineering → Translator writing systems and compiler generators
|
|
URL: https://hal.inria.fr/hal-03518825/file/Rabit_TOSEM.pdf
https://hal.inria.fr/hal-03518825/document
https://doi.org/10.1145/3409805
https://hal.inria.fr/hal-03518825
|
|
BASE
|
|
Hide details
|
|
|
| 2 |
A sequent calculus with dependent types for classical arithmetic
|
|
|
|
In: LICS 2018 - 33th Annual ACM/IEEE Symposium on Logic in Computer Science ; https://hal.inria.fr/hal-01703526 ; LICS 2018 - 33th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2018, Oxford, United Kingdom. pp.720-729, ⟨10.1145/3209108.3209199⟩ (2018)
|
|
BASE
|
|
Show details
|
|
|
| 3 |
A Generic Framework for Symbolic Execution: a Coinductive Approach
|
|
|
|
In: ISSN: 0747-7171 ; EISSN: 1095-855X ; Journal of Symbolic Computation ; https://hal.inria.fr/hal-01238696 ; Journal of Symbolic Computation, Elsevier, 2017, 80, pp.125-163. ⟨10.1016/j.jsc.2016.07.012⟩ (2017)
|
|
BASE
|
|
Show details
|
|
|
| 4 |
Quelques ponts entre sémantique opérationnelle et modèles dénotationnels des langages de programmation
|
|
|
|
In: https://hal.archives-ouvertes.fr/tel-01400666 ; Logique en informatique [cs.LO]. Université Grenoble Alpes, 2016 (2016)
|
|
BASE
|
|
Show details
|
|
|
| 5 |
Dynamische Modellanalyse von Metamodellen mit operationaler Semantik
|
|
Soden, Michael. - : Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II, 2015
|
|
BASE
|
|
Show details
|
|
|
| 6 |
Dynamische Modellanalyse von Metamodellen mit operationaler Semantik ...
|
|
Soden, Michael. - : Humboldt-Universität zu Berlin, Mathematisch-Naturwissenschaftliche Fakultät II, 2015
|
|
BASE
|
|
Show details
|
|
|
| 7 |
Operational Semantics of the Model of Concurrency and Communication Language
|
|
|
|
In: https://hal.inria.fr/hal-01060601 ; [Research Report] RR-8584, INRIA. 2014, pp.23 (2014)
|
|
BASE
|
|
Show details
|
|
|
| 8 |
Nested atomic sections with thread escape : semantics and compilation ; Sections atomiques emboîtées avec échappement de processus légers : sémantiques et compilation
|
|
|
|
In: https://tel.archives-ouvertes.fr/tel-01362118 ; Algorithme et structure de données [cs.DS]. Université d'Orléans, 2014. Français. ⟨NNT : 2014ORLE2075⟩ (2014)
|
|
BASE
|
|
Show details
|
|
|
| 9 |
Specifying and verifying program transformations with PTRANS
|
|
|
|
BASE
|
|
Show details
|
|
|
| 10 |
situ-f: a domain specific language and a first step towards the realization of situ framework
|
|
|
|
In: Graduate Theses and Dissertations (2012)
|
|
BASE
|
|
Show details
|
|
|
| 11 |
Formally Tracing Executions From an Analysis Tool Back to a Domain Specific Modeling Language's Operational Semantics
|
|
|
|
In: https://hal.inria.fr/inria-00526561 ; [Research Report] RR-7423, INRIA. 2010 (2010)
|
|
BASE
|
|
Show details
|
|
|
| 12 |
Rule Formats for Determinism and Idempotence
|
|
|
|
In: http://www.ru.is/faculty/luca/PAPERS/SCP-idempotence.pdf (2010)
|
|
BASE
|
|
Show details
|
|
|
| 13 |
Graph transformation systems in Constraint Handling Rules: improved methods for program analysis ...
|
|
|
|
BASE
|
|
Show details
|
|
|
| 15 |
Peter, the Language that does not Exist. ; Peter, le langage qui n’existe pas.
|
|
|
|
In: https://hal.inria.fr/tel-01148503 ; Computation and Language [cs.CL]. INPL - INP de LORRAINE, 2007 (2007)
|
|
BASE
|
|
Show details
|
|
|
| 16 |
Words Mean Things: What is the Decisive Point?
|
|
|
|
In: DTIC (2007)
|
|
BASE
|
|
Show details
|
|
|
| 17 |
A Hierarchy of SOS Rule Formats
|
|
|
|
In: http://www.win.tue.nl/~mousavi/sos05_invited.pdf (2005)
|
|
BASE
|
|
Show details
|
|
|
| 18 |
A GH-Based Ontology to Support Applications for Automating Decision Support
|
|
|
|
In: DTIC (2005)
|
|
BASE
|
|
Show details
|
|
|
| 19 |
A Formal Syntax and Semantics for the GSPML Language
|
|
|
|
In: DTIC AND NTIS (2005)
|
|
BASE
|
|
Show details
|
|
|
| 20 |
Semantics of the reFLect Language
|
|
|
|
In: http://www.cse.ogi.edu/~johnm/papers/KrsticMatthews_04.pdf (2004)
|
|
BASE
|
|
Show details
|
|
|
|
|
