Ivannikov Institute for System Programming of the RAS

Minimizing the number of static verifier traces to reduce time for finding bugs in Linux kernel modules.


V. Mordan, E. Novikov.


Static verifiers usually stop after they find a first bug in a program under analysis. This slows down the process of finding and fixing of bugs of the same kind in a given Linux kernel module. In order to solve this problem we used the static verifier CPAchecker with option to continue analysis after finding of a first bug. Besides we extended LDV Tools – a toolset for verification of Linux kernel modules – for finding several bugs in a given module against a specified rule specification. But first experiments revealed a new problem – the verifier produced too many similar traces. The given paper introduces a formal definition of equivalent traces and presents different comparison algorithms and a semi-automated approach, which makes possible to find several bugs in a given Linux kernel module against a specified rule specification at once.

Full text of the paper in pdf


Linux kernel module; correctness rule; static verifier trace; equivalence class


Proceedings of the 8th Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE 2014), editors A. Kamkin, A. Petrenko, A. Terekhov, Saint Petersburg, Russia, May 29-31. ISP RAS, Moscow, 2014.

DOI: 10.15514/SYRCOSE-2014-8-5


Research Group

Software Engineering

All publications during 2014 All publications