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


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

Денис Ефремов. Начало семинара - 26 марта 2013 г.

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

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

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

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

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