Detecting Non-cyclicity by Abstract Compilation into Boolean Functions.

Programming languages such as C, C++ and Java bind variables to dynamically-allocated data-structures held in memory. This lets programs build cyclical data at run-time, which complicates termination analysis and garbage collection. It is hence desirable to spot those variables which are only bound to non-cyclical data at run-time. We solve this problem by using abstract interpretation to define the abstract domain representing those variables. We relate through a Galois insertion to the concrete domain of program states. Hence is not redundant. We define a correct abstract denotational semantics over , which uses preliminary sharing information between variables to get more precise results. We apply it to a simple example of analysis. We use a Boolean representation for the abstract denotations over , which leads to an efficient implementation in terms of binary decision diagrams and to the elegant and efficient use of abstract compilation. [ABSTRACT FROM AUTHOR]