How to cook an automated system for Linux driver verification.

Authors

Khoroshilov A., Mutilin V., Shcherbina V., Strikov O., Vinogradov S., Zakharov V.A.

Abstract

Abstract—We present the preliminary results of our work on designing an automatic toolset for verification of Linux kernelspace drivers. By now the toolset includes three components:
• a library of verification models; each model is a formal description of some safety property to be checked;
• a preprocessor unit; it is intended for simulating an environment of a driver;
• a verification unit BLAST; it is a general-purpose toolkit intended for automatic program verification based on Boolean abstraction and counter-example guided abstraction refinements techniques.
We discuss in some details how our system operates and outline the directions for future work.

Edition

Proceedings of the 1st Spring Young Researchers’ Colloquium on Software Engineering SYRCoSE 2008 (St Petersburg, May 29-30, 2008), 2008, Санкт-Петербург, с. 15-19.

Research Groups

Software Engineering, Theoretical Computer Science

All publications during 2008

All publications