How to Cook an Automated System for Linux Driver Verification.


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 год Все публикации