Expression-Based Aliasing for OO-languages
METADATA ONLY
Loading...
Author / Producer
Date
2015
Publication Type
Conference Paper
ETH Bibliography
yes
Citations
Altmetric
METADATA ONLY
Data
Rights / License
Abstract
Alias analysis has been an interesting research topic in verification and optimization of programs. The undecidability of determining whether two expressions in a program may reference to the same object is the main source of the challenges raised in alias analysis. In this paper we propose an extension of a previously introduced alias calculus based on program expressions, to the setting of unbounded program executions such as infinite loops and recursive calls. Moreover, we devise a corresponding executable specification in the \(\mathbb {K}\)-framework. An important property of our extension is that, in a non-concurrent setting, the corresponding alias expressions can be over-approximated in terms of a notion of regular expressions. This further enables us to show that the associated \(\mathbb {K}\)-machinery implements an algorithm that always stops and provides a sound over-approximation of the “may aliasing” information, where soundness stands for the lack of false negatives. As a case study, we analyze the integration and further applications of the alias calculus in SCOOP. The latter is an object-oriented programming model for concurrency, recently formalized in Maude; \(\mathbb {K}\) definitions can be compiled into Maude for execution.
Permanent link
Publication status
published
External links
Book title
Formal Techniques for Safety-Critical Systems
Journal / series
Volume
476
Pages / Article No.
47 - 61
Publisher
Springer
Event
3rd International Workshop on Formal Techniques for Safety-Critical Systems (FTSCS 2014)