Expression-Based Aliasing for OO–languages

DOI10.1007/978-3-319-17581-2_4MaRDI QIDQ3460212zbMATH OpenOpenAlexFDO

Publication date 6 January 2016

Published in Communications in Computer and Information Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1409.7509

Theory of programming languages (68N15) Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19)

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 s.a. infinite loops and recursive calls. Moreover, we devise a corresponding executable specification in the 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 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; K-definitions can be compiled into Maude for execution.

Recommendations

Cites work

Cited in

(5)

Describes a project that uses

Uses Software

This page was built for publication: Expression-Based Aliasing for OO–languages

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3460212)