Alias Analysis by Means of a Model Checker

9 years 11 months ago
Alias Analysis by Means of a Model Checker
We study the application of a standard model checker tool, Spin, to the well-known problem of computing a may-alias relation for a C program. A precise may-alias relation can significantly improve code optimization, but in general it may be computationally too expensive. We show that, at least in the case of intraprocedural alias analysis, a model checking tool has a great potential for precision and efficiency. For instance, we can easily deal, with good precision, with features such as pointer arithmetic, arrays, structures and dynamic memory allocation. At the very least, the great flexibility allowed in defining the may-alias relation, should make it easier to experiment and to examine the connections among the accuracy of an alias analysis and the optimizations available in the various compilation phases.
Vincenzo Martena, Pierluigi San Pietro
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Where CC
Authors Vincenzo Martena, Pierluigi San Pietro
Comments (0)