A Pointer Logic Dealing with Uncertain Equality of Pointers

We have designed a pointer logic for a C-like programming language PointerC. The pointer logic is an extension of Hoare logic, and it uses the idea of precise alias analysis in pointer program verification to support safety verification of programs in which equality of pointers is well-regulated. In this work, we present an extension to the pointer logic by introducing a set of uncertain-equality pointer access path sets, so that we can reason in the extended pointer logic about properties of programs which manipulate data structures like directed graph in which equality of pointers