Abstract: Verifying program by formal method is an important way to ensure software trusted. For low level imperative language like C language which can operate memory directly, a suitable memory model is needed to formalize the operational semantics or axiomatic semantics. The traditional byte memory model can describe various memory operations very well, however, it cant guarantee safety and make program-verifying complex. The memory model of object-oriented language is high-level. It is suitable for program verification but not for describing low level memory operation. A safe typed memory model is proposed by combining the previous two kind models. It can be used to formalize semantics and to verify program based on Hoare logic. This memory model allows pointer arithmetic, structure assignment, type cast and other memory operations, and makes pointer-based programs verification easier. The memory model is formalized and verified using Coq proof assistant.