BLASTing Linux Code
Jan Tobias Mühlberg and
Gerald Lüttgen
Department of Computer Science, University of York, York YO10 5DD, U.K.
main page
This web site contains additional material regarding the paper
"BLASTing Linux Code" presented at
FMICS 2006.
It currently contains the source code used in our case studies but
lacks manual simplifications and temporal safety specifications.
Abstract and Paper
Abstract. Computer programs can only run reliably if the underlying
operating system is free of errors. In this paper we evaluate, from a
practitioners point of view, the utility of the popular software model
checker BLAST for revealing errors in Linux kernel code. The emphasis is
on important errors related to memory safety in and locking behaviour
of device drivers. Our conducted case studies show that, while BLAST's
abstraction and refinement techniques are efficient and powerful, the tool
has deficiencies regarding usability and support for analysing pointers,
which are likely to prevent kernel developers from using it.
|
Full paper: blasting_linux_code.pdf
(450 kBytes)
BibTeX: blasting_linux_code.bib
Presentation slides: slides.pdf (450 kBytes)
|
Technical Report: YCS-2007-417.pdf
(516 kBytes)
BibTeX: YCS-2007-417.bib
|
Examples Regarding Memory Safety
Examples Regarding Locking Properties
Jan Tobias Mühlberg, $Date$
|