Abstract: Lots of dynamitic memories are used in Java program．The unreachable dynamitic memories can be collected by the garbage collector．The reachable but inactive dynamitic memories are free which may lead to memory leak．The bi-deduction method to detect memory leak in Java program is provided．It is based on separation logic．By using separation logic and the rules of Hoare logic,the dynamitic memory’s state can be achieved and the leaked memory can be detected.

Key words: Memory leak,Separation logic,Bi-deduction,Inference rule of hoare logic