Model checking concurrent linux device drivers
The SLAM toolkit demonstrates that predicate abstraction enables automated verification of real world Windows device drivers. 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. W...
| Päätekijät: | , , , |
|---|---|
| Muut tekijät: | |
| Aineistotyyppi: | Conference item |
| Julkaistu: |
Association for Computing Machinery
2007
|