loading...
 This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
30th Annual IEEE/NASA Software Engineering Workshop SEW-30 (SEW'06)
Detecting Deadlock, Double-Free and Other Abuses in a Million Lines of Linux Kernel Source
Columbia, Maryland
April 24-April 28
ISBN: 0-7695-2624-1
ASCII Text
x 
 
Peter T. Breuer, Simon Pickin, Maria Larrondo Petrie, "Detecting Deadlock, Double-Free and Other Abuses in a Million Lines of Linux Kernel Source," Software Engineering Workshop, Annual IEEE/NASA Goddard, pp. 223-233, 30th Annual IEEE/NASA Software Engineering Workshop SEW-30 (SEW'06), 2006.
 
 
BibTex
x
 
@article{ 10.1109/SEW.2006.15,
author = {Peter T. Breuer and Simon Pickin and Maria Larrondo Petrie},
title = {Detecting Deadlock, Double-Free and Other Abuses in a Million Lines of Linux Kernel Source},
journal ={Software Engineering Workshop, Annual IEEE/NASA Goddard},
volume = {0},
year = {2006},
issn = {1550-6215},
pages = {223-233},
doi = {http://doi.ieeecomputersociety.org/10.1109/SEW.2006.15},
publisher = {IEEE Computer Society},
address = {Los Alamitos, CA, USA},
}
 
 
RefWorks Procite/RefMan/Endnote
x 
 
TY - CONF
JO - Software Engineering Workshop, Annual IEEE/NASA Goddard
TI - Detecting Deadlock, Double-Free and Other Abuses in a Million Lines of Linux Kernel Source
SN - 1550-6215
SP223
EP233
A1 - Peter T. Breuer,
A1 - Simon Pickin,
A1 - Maria Larrondo Petrie,
PY - 2006
KW - null
VL - 0
JA - Software Engineering Workshop, Annual IEEE/NASA Goddard
ER -
 
Peter T. Breuer, Universidad Carlos III de Madrid, Spain; Florida Atlantic University, USA
Simon Pickin, Universidad Carlos III de Madrid, Spain; Florida Atlantic University, USA
Maria Larrondo Petrie, Universidad Carlos III de Madrid, Spain; Florida Atlantic University, USA
The formal analysis described here detects two so far undetected real deadlock situations per thousand C source files or million lines of code in the open source Linux operating system kernel, and three undetected accesses to freed memory, at a few seconds per file. That is notable because the code has been continuously under scrutiny from thousands of developers? pairs of eyes. In distinction to model-checking techniques, which also use symbolic logic, the analysis uses a "3-phase" compositional Hoare-style programming logic combined with abstract interpretation. The result is a customisable post-hoc semantic analysis of C code that is capable of several different analyses at once.
Citation:
Peter T. Breuer, Simon Pickin, Maria Larrondo Petrie, "Detecting Deadlock, Double-Free and Other Abuses in a Million Lines of Linux Kernel Source," sew, pp.223-233, 30th Annual IEEE/NASA Software Engineering Workshop SEW-30 (SEW'06), 2006
Usage of this product signifies your acceptance of the Terms of Use.