Using Linux Device Drivers for Static Verification Tools Benchmarking.

Authors

M. U. Mandrykin, V. S. Mutilin, E. M. Novikov, A. V. Khoroshilov, and P. E. Shved.

Abstract

The Linux Driver Verification system is designed for static analysis of the source code of Linux kernel space device drivers. In this paper, we describe the architecture of the verification system, including the integration of third-party tools for static verification of C programs. We consider characteristics of the Linux drivers source code that are important from the viewpoint of verification algorithms and give examples of comparative analysis of different verification tools, as well as different versions and configurations of a given tool.

Edition

Programming and Computer Software, 2012, Volume 38, Number 5, Pages 245-256.

DOI: 10.1134/S0361768812050039

Research Group

Software Engineering

All publications during 2012

All publications