From Uncertainty to Belief: Inferring the Specification Within

Automatic tools for finding software errors require a set of specifications before they can check code: if they do not know what to check, they cannot find bugs. This paper presents a novel framework based on factor graphs for automatically inferring specifications directly from programs. The key strength of the approach is that it can incorporate many disparate sources of evidence, allowing us to squeeze significantly more information from our observations than previously published techniques. We illustrate the strengths of our approach by applying it to the problem of inferring what functions in C programs allocate and release resources. We evaluated its effectiveness on five codebases: SDL, OpenSSH, GIMP, and the OS kernels for Linux and Mac OS X (XNU). For each codebase, starting with zero initially provided annotations, we observed an inferred annotation accuracy of 80-90%, with often near perfect accuracy for functions called as little as five times. Many of the inferred allocat...

• Type: Conference
• Year: 2006
• Where: OSDI
• Authors: Ted Kremenek, Paul Twohey, Godmar Back, Andrew Y. Ng, Dawson R. Engler
• Keywords: Inferred Allocator, Inferred Annotation Accuracy, Inferred Annotations, Operating System, OSDI 2006