Model checking concurrent linux device drivers

Thomas Witkowski, Nicolas Blanc, Daniel Kroening, Georg Weissenbacher

Abstract

The S lam toolkit demonstrates that predicate abstraction enables automated verification of real world Windows device drivers. Our predicate abstraction-based tool DDV erify enables the automated verification of Linux device drivers and provides an accurate model of the relevant parts of the kernel. We report on benchmarks based on Linux device drivers, confirming the results that S lam established for the Windows world. Furthermore, we take predicate abstraction one step further and introduce a technique to verify concurrent software with shared memory

BibTeX

@inproceedings{Witkowski-al:ASE07,
  author    = {Thomas Witkowski and
               Nicolas Blanc and
               Daniel Kroening and
               Georg Weissenbacher},
  title     = {Model checking concurrent linux device drivers},
  booktitle = {ASE},
  pages     = {501--504},
  publisher = {{ACM}},
  year      = {2007},
}

Model checking concurrent linux device drivers

Abstract

Related papers