Нахождение всех ошибок в модулях ядра Linux за один запуск верификатора

Мордань Виталий. Начало семинара - 02 апреля 2014 г.

Современные статические верификаторы используются только для поиска первой встретившейся ошибки для лишь одного выбранного правила корректности. В результате процесс нахождения всех ошибок в ядре Linux оказывается очень долгим. В настоящей работе предлагается идея мульти-аспектной верификации, а также представлены первые эксперименты в области нахождения всех нарушений выбранного правила с помощью инструментов LDV Tools и статического верификатора CPAchecker.

С презентацией доклада можно ознакомиться здесь.

Семинар группы

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

Перейти к списку семинаров ИСП РАН