Abstract: In C language that support dynamic memory operations, the usage of pointer brings about memory leak which is the key factor that causes system performance degradation.For the inadequacy of existing approaches, a method of static detection to memory leak based on model checking was proposed in this paper.By modeling memory leak vulnerabilities based on the attributes of a pointer, the method instrument the source code with corresponding constraint assertions, and then verify the reachability of these assertions by model checking tools.Experimental results show that the method is effective and accurate.