Memory Leak Analysis by Contradiction
Maksim Orlovich (Cornell University) and Radu Rugina (Cornell University)
Abstract
We present a novel leak detection algorithm. To prove the absence of a memory leak, the algorithm assumes its presence and runs a reverse heap analysis to disprove this assumption. We have implemented this algorithm in a memory leak analysis tool and used it to verify several heap-intensive manipulation programs. Because of the reverse nature of the algorithm, for many codes it is able to locally prove the absence of leaks, or to compute preconditions for unsafe operation without needing to analyze the entire source to the program.