A Smooth Combination of Linear and Herbrand Equalities for Polynomial Time Must-Alias Analysis

Abstract. 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.

• Type: Conference
• Year: 2009
• Where: FM
• Authors: Helmut Seidl, Vesal Vojdani, Varmo Vene
• Keywords: Address Expressions, Assertion Checking Algorithms, FM 2009, Natural Language Processing, Smooth Combination