Checking for deadlock, double-free and other abuses in the Linux kernel source code

Abstract

The analysis described in this article detects about two real and uncorrected deadlock situations per thousand C source files or million lines of code in the Linux kernel source, and three accesses to freed memory, at a few seconds per file. In distinction to model-checking techniques, the analysis applies a configurable "3-phase" Hoare-style logic to an abstract interpretation of C code to obtain its results. © Springer-Verlag Berlin Heidelberg 2006.