Links und Funktionen

You are here: Home / Publikationen / Verifying Pointer and String Analyses with Region Type Systems


Lennart Beringer, Robert Grabowski, and Martin Hofmann (2010)

Verifying Pointer and String Analyses with Region Type Systems

In: LPAR (Dakar), pp. 82-102.

Pointer analysis statically approximates the heap pointer structure during a program execution in order to track heap objects or to establish alias relations between references, and$~$ usually contributes to other analyses or code optimizations. In recent years, a number of algorithms have been presented that provide an efficient, scalable, and yet precise pointer analysis.$~$ However, it is unclear how the results of these algorithms compare to each other semantically. In this paper, we present a general region type system for a Java-like language and give a$~$ formal soundness proof. The system is subsequently specialized to obtain a platform for embedding the results of various existing context-sensitive pointer analysis algorithms, thereby$~$ equipping the computed relations with a common interpretation and verification. We illustrate our system by outlining an extension to a string value analysis that builds on pointer$~$ information.

Document Actions