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$