TY - GEN
T1 - Verifying pointer and string analyses with region type systems
AU - Beringer, Lennart
AU - Grabowski, Robert
AU - Hofmann, Martin
PY - 2010
Y1 - 2010
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=78650816912&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=78650816912&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-17511-4_6
DO - 10.1007/978-3-642-17511-4_6
M3 - Conference contribution
SN - 3642175104
SN - 9783642175107
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 82
EP - 102
BT - Logic for Programming, Artificial Intelligence, and Reasoning - 16th International Conference, LPAR-16, Revised Selected Papers
T2 - 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning, LPAR-16
Y2 - 25 April 2010 through 1 May 2010
ER -