Saved in:
| Main Authors: | , |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | https://arxiv.org/abs/2406.16063 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866912195463348224 |
|---|---|
| author | Amato, Gianluca Scozzari, Francesca |
| author_facet | Amato, Gianluca Scozzari, Francesca |
| contents | Static analysis of logic programs by abstract interpretation requires designing abstract operators which mimic the concrete ones, such as unification, renaming and projection. In the case of goal-driven analysis, where goal-dependent semantics are used, we also need a backward-unification operator, typically implemented through matching. In this paper we study the problem of deriving optimal abstract matching operators for sharing and linearity properties. We provide an optimal operator for matching in the domain ${\mathtt{ShLin}^ω}$, which can be easily instantiated to derive optimal operators for the domains ${\mathtt{ShLin}^{2}}$ by Andy King and the reduced product $\mathtt{Sharing} \times \mathtt{Lin}$. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2406_16063 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Optimal matching for sharing and linearity analysis Amato, Gianluca Scozzari, Francesca Programming Languages Logic in Computer Science 68N17, 68N30 D.1.6; D.2.4 Static analysis of logic programs by abstract interpretation requires designing abstract operators which mimic the concrete ones, such as unification, renaming and projection. In the case of goal-driven analysis, where goal-dependent semantics are used, we also need a backward-unification operator, typically implemented through matching. In this paper we study the problem of deriving optimal abstract matching operators for sharing and linearity properties. We provide an optimal operator for matching in the domain ${\mathtt{ShLin}^ω}$, which can be easily instantiated to derive optimal operators for the domains ${\mathtt{ShLin}^{2}}$ by Andy King and the reduced product $\mathtt{Sharing} \times \mathtt{Lin}$. |
| title | Optimal matching for sharing and linearity analysis |
| topic | Programming Languages Logic in Computer Science 68N17, 68N30 D.1.6; D.2.4 |
| url | https://arxiv.org/abs/2406.16063 |