Using linux device drivers for static verification tools benchmarking
Mikhail Usamovich Mandrykin, Vadim Mutilin, Evgeny Novikov, Alexey Vladimirovich Khoroshilov, Pavel Shved · Programming and Computer Software · 2012
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.