Abstract: Formal verification is a major method to improve the dependability of software. One of the hot research areas is automatic program verification based on logical inference. So far there is no product which can be used directly in the industries, and the root of this problem lies in the slow development and difficulties of automated theorem proving. Our approach is based on the observation that program analysis methods can be used in collecting global information to support program verification. We build shape graphs at each program point in the program analysis phase. A method is proposed, which uses regular Hoare logic rules to reason about assignment not dealing with pointers in a C-like programming language. Such rules will be applied after aliasing is eliminated using the information of shape graphs. The soundness of the logic system has been proved. Furthermore, an approach is presented to verify data constraints on mutable data structures without using user-defined predicates. A prototype of our program verifier has been implemented for the PointerC programming language. We have used it in the verification of programs manipulating recursive data structures, such as lists and trees, and programs dealing with one-dimension arrays.