|
ИСТИНА |
Войти в систему Регистрация |
ИСТИНА ЦЭМИ РАН |
||
Minimizing the Number of Static Verifier Traces to Reduce Time for Finding Bugs in Linux Kernel Modulesстатья
- Авторы: Mordan Vitaly, Novikov Evgeny
- Сборник: Proceedings of the 8th Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE 2014)
- Год издания: 2014
- DOI: 10.15514/syrcose-2014-8-5
- Аннотация: 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.
- Добавил в систему: Мордань Виталий Олегович