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.