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

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.

Полный текст статьи в формате 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


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

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

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