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.
CITATION STYLE
Breuer, P. T., & Pickin, S. (2006). Checking for deadlock, double-free and other abuses in the Linux kernel source code. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3994 LNCS-IV, pp. 765–772). Springer Verlag. https://doi.org/10.1007/11758549_103
Mendeley helps you to discover research relevant for your work.