Sciweavers

Share
KBSE
2007
IEEE

Model checking concurrent linux device drivers

8 years 10 months ago
Model checking concurrent linux device drivers
toolkit demonstrates that predicate abstraction enables automated verification of real world Windows device Our predicate abstraction-based tool DDVerify 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 Slam established for the Windows world. Furthermore, we take predicate abstraction one step further and introduce a technique to verify concurrent software with shared memory. Categories and Subject Descriptors:D.2.4[Software Engineering]: Program Verification; D.4.5[Operating Systems]: Reliability General Terms: Verification, Reliability
Thomas Witkowski, Nicolas Blanc, Daniel Kroening,
Added 04 Jun 2010
Updated 04 Jun 2010
Type Conference
Year 2007
Where KBSE
Authors Thomas Witkowski, Nicolas Blanc, Daniel Kroening, Georg Weissenbacher
Comments (0)
books