Институт системного программирования им. В.П. Иванникова РАН

How to Cook an Automated System for Linux Driver Verification.


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


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.

Полный текст статьи в формате pdf (на английском)


St. Petersburg, ISP RAS, In Proceedings of the Second Spring Young Researchers’ Colloquium on Software Engineering (SYRCoSE’2008), 2008, Vol 2, pp. 11-14.

DOI: 10.15514/SYRCOSE-2008-2-14

ISBN 978-5-91474-006-8

Научная группа

Технологии программирования

Все публикации за 2008 год Все публикации