The location linking concept: a basis for verification of code using pointers

While the use of pointers can be minimized by language mechanisms for data abstraction, alias avoidance and control, and disciplined software development techniques, ultimately, any verifying compiler effort must be able to verify code that makes use of them. Additionally, in order to scale, the verification machinery of such a compiler must use specifications to reason about components. This paper follows a natural question that arises from combining these ideas: can the general machinery of specification-based component verification also be used to verify code that uses instances of types that are more traditionally built-in, such as arrays and pointers? This paper answers the question in the affirmative by presenting a Location_Linking_Template, a concept that captures pointer behavior, and uses it to verify the code of a simple data abstraction realized using pointers. In this deployment, pointers have a specification like any other component. We also note that the concept can be extended and realized so that different systems can plug in alternative implementations to give programmers the flexibility to choose, e.g., manual memory management or automatic garbage collection depending on their performance concerns.