Static memory leak detection

Memory management problems are common in programs written in languages requiring manual memory deallocation. They are important because they can cause program failure, potentially allowing remote denial of service or unauthorized execution. This dissertation presents a novel static analysis and its implementation Clouseau, a tool that can semi-automatically identify memory leaks and double deletes in large C and C++ applications.; We have formalized a practical ownership model of memory management and developed type systems to enforce it. In the model, every object is pointed to by one and only one owning pointer, which holds the exclusive right and obligation to either delete the object or to transfer the right to another owning pointer.; Programs hold references to many objects in container data structures like lists and maps. Some containers have polymorphic element ownership and can be used to hold either owning or non-owning pointers to objects. Clouseau helps identify containers in large programs. Small user-generated specifications on the procedures that manipulate containers are then used to enforce the ownership model.; Clouseau uses flow-sensitive and context-sensitive algorithms to infer likely ownership interfaces of procedures, methods, and object fields. Statements inconsistent with the model are identified as sources of potential errors. The algorithms are sound with respect to a large subset of the C and C++ languages, reporting warnings for all possible errors. They are practical and useful; identifying those warnings likely corresponding to errors and aiding user understanding by identifying inferred ownership interfaces.; Applying Clouseau to ten applications demonstrates its applicability to large real programs and its effectiveness at finding memory management problems. We show that enforcing ownership models is efficient and effective at identifying leaks and multiple deletions in important programs and libraries. We compare identifying leaks statically using Clouseau to identifying them dunamically; in many cases, our system finds program errors that account for a large majority of the dynamic memory leak volume. Moreover, where no leaks were identified dynamically, Clouseau found potential leaks. Clouseau is effective at identifying container implementations in large programs. Modeling ownership in containers can substantially increase the effectiveness of static leak detection.