Pointer is an important data type in most programming languages.It can make programs more efficient and more elegant.Unfortunately,this important concept is always notorious for its timelessness.Until now,no proper way to formalize it in temporal logic language has been found.XYZ/E is a temporal logic system as well as a programming language.It can represent almost every kind of significant features in conventional imperative languages.This paper is devoted to the representation of pointer in language XYZ/E and the verification of XYZ/SE programs with pointers.