TY - GEN
T1 - A smooth combination of linear and herbrand equalities for polynomial time must-alias analysis
AU - Seidl, Helmut
AU - Vojdani, Vesal
AU - Vene, Varmo
PY - 2009
Y1 - 2009
N2 - We present a new domain for analyzing must-equalities between address expressions. The domain is a smooth combination of Herbrand and affine equalities which enables us to describe field accesses and array indexing. While the full combination of uninterpreted functions with affine arithmetics results in intractable assertion checking algorithms, our restricted domain allows us to construct an analysis of address must-equalities that runs in polynomial time. We indicate how this analysis can be applied to infer access patterns in programs manipulating arrays and structs.
AB - We present a new domain for analyzing must-equalities between address expressions. The domain is a smooth combination of Herbrand and affine equalities which enables us to describe field accesses and array indexing. While the full combination of uninterpreted functions with affine arithmetics results in intractable assertion checking algorithms, our restricted domain allows us to construct an analysis of address must-equalities that runs in polynomial time. We indicate how this analysis can be applied to infer access patterns in programs manipulating arrays and structs.
UR - http://www.scopus.com/inward/record.url?scp=70649099069&partnerID=8YFLogxK
U2 - 10.1007/978-3-642-05089-3_41
DO - 10.1007/978-3-642-05089-3_41
M3 - Conference contribution
AN - SCOPUS:70649099069
SN - 3642050883
SN - 9783642050886
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 644
EP - 659
BT - FM 2009
T2 - 2nd World Congress on Formal Methods, FM 2009
Y2 - 2 November 2009 through 6 November 2009
ER -