Статико-динамическая верификация драйверов файловых систем ядра Linux

Денис Ефремов. Начало семинара - 14 мая 2014 г.

На семинаре будет рассмотрен метод concolic тестирования и его применение для верификации модулей ядра ОС GNU/Linux. Будет рассказано об использовании особенностей реализации драйверов файловых систем для осуществления данного вида тестирования. А также рассмотрен вопрос автоматического создания тестовых образцов файловых систем. Concolic (от англ конкретный и символический) тестирование представляет собой гибридный метод верификации программного обеспечения, который чередует конкретное исполнение (исполнение с определёнными входными данными) с символическим исполнением. Последнее рассматривает переменные программы как символические переменные. Символическое исполнение используется в сочетании со средством автоматизированного доказательства теорем для создания новых конкретных входных данных с целью максимального покрытия кода.

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

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

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