2018/08/27 by Víctor Rivera, Bertrand Meyer, Rivera, Victor +1 · 1 citation
Computer Science · #FOS: Computer and information sciences #Formal Methods in Verification #Logic, programming, and type systems #Software Engineering (cs.SE) #Software Testing and Debugging Techniques
paper · pdf · doi:10.48550/arxiv.1808.08748
openalex publication_date 2018/08/27 · openalex created_date 2022/08/03 · openalex updated_date 2026/07/28
The aliasing question (can two reference expressions point, during an\nexecution, to the same object?) is both one of the most critical in practice,\nfor applications ranging from compiler optimization to programmer verification,\nand one of the most heavily researched, with many hundreds of publications over\nseveral decades. One might then expect that good off-the-shelf solutions are\nwidely available, ready to be plugged into a compiler or verifier. This is not\nthe case. In practice, efficient and precise alias analysis remains an open\nproblem.\n We present a practical tool, AutoAlias, which can be used to perform\nautomatic alias analysis for object-oriented programs. Based on the theory of\n"duality semantics", an application of Abstract Interpretation ideas, it is\ndirected at object-oriented languages and has been implemented for Eiffel as an\naddition to the EiffelStudio environment. It offers variable-precision\nanalysis, controllable through the choice of a constant that governs the number\nof fix point iterations: a higher number means better precision and higher\ncomputation time.\n All the source code of AutoAlias, as well as detailed results of analyses\nreported in this article, are publicly available. Practical applications so far\nhave covered a library of data structures and algorithms and a library for GUI\ncreation. For the former, AutoAlias achieves a precision appropriate for\npractical purposes and execution times in the order of 25 seconds for about\n8000 lines of intricate code. For the GUI library, AutoAlias produces the alias\nanalysis in around 232 seconds for about 150000 lines of intricate code.\n