Аспирант Захаров Илья Сергеевич

Захаров Илья Сергеевич

Направление подготовки: 09.06.01 «Информатика и вычислительная техника».
Направленность (специальность): 05.13.11 «Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей».
Дата зачисления: 01 октября 2014 года.
Приказ о зачислении: 10-у от 30.09.2014 года.
Срок окончания аспирантуры: 30 сентября 2018 года.
Форма обучения: очная.

Экзамены

Педагогика высшей школы: отлично, июнь 2016 года.

Кандидатские экзамены

Иностранный язык: отлично, 08.06.2015.
История и философия науки: отлично, 23.06.2015.
Специальность 05.13.11: отлично, 1 июня 2016 года.

Достижения в научно-исследовательской деятельности

Тема диссертационного исследования: Методы оптимизации статической верификации.
Утверждена на заседании Учёного совета ИСП РАН: Протокол №2014-13 от 26.12.2014 года.
Научный руководитель: Петренко Александр Константинович, д.ф.-м.н. профессор, руководитель отдела «Технологии программирования».

Сведения о планируемой диссертационной работе

Для верификации модулей ядра Linux при помощи инструментов статической верификации исходного кода требуется большое количество вычислительных ресурсов. Данная работа нацелена на сокращение требований к объему оперативной памяти и процессорного времени необходимых для верификации драйверов ядра Linux, включая те, объем исходного кода которых превышает 100 тыс. строк кода. При этом требуется не допустить снижения точности анализа инструментами верификации, чтобы не возросло число ложных сообщений об ошибках и число пропущенных ошибок.

Данные об участии в фундаментальных научных исследованиях, программах и грантах

1. Разработка методов и инструментов для масштабируемой статической верификации системного программного обеспечения, № госрегистрации - 114121550037. Результат: Разработка метода и инструментов для масштабируемой статической верификации модулей ядра Linux.
2. Разработка адаптивных методов статического анализа с моделями памяти повышенной точности, № госрегистрации - 115012770061. Результат: Разработка адаптивных методов статического анализа модулей ядра Linux.

Информация об участии в конференциях различного уровня

1. LDV workshop 2015, г. Москва, октябрь 2015. Участие: очное с докладом, без публикации.
2. Ershov Informatics Conference, г. Санкт-петербург, июнь 2014. Участие: очное с докладом и публикацией.

Список опубликованных научных и учебно-методических работ

1. Моделирование окружения с использованием шаблонов для статической верификации модулей ядра Linux. В.С. Мутилин, А.В. Хорошилов, Захаров И.С. Журнал Программирование, том 41, выпуск 3, стр. 183-195, 2015.
2. Конфигурируемая система статической верификации модулей ядра операционных систем. М.У. Мандрыкин, В.С. Мутилин, Е.М. Новиков, А.К. Петренко, А.В. Хорошилов. Труды Института системного программирования РАН, том 26, 2014 г. Выпуск 2.
3. Modeling Environment for Static Verification of Linux Kernel Modules. В.С. Мутилин, Е.М. Новиков, А.В. Хорошилов, Захаров И.С. Lecture Notes in Computer Science, Volume 8974, 400-414.
4. "Configurable toolset for static verification of operating systems kernel modules". I.S. Zakharov, M.U. Mandrykin, V.S. Mutilin, E.M. Novikov, A.K. Petrenko, A.V. Khoroshilov. Programming and Computer Software 41.1 (Jan. 2015), pp. 49–64. doi: 10.1134/S0361768815010065.
5. «Инкрементальное построение спецификаций моделей окружения и требований для подсистем монолитного ядра операционных систем». И.С. Захаров и Новиков Е.М. Труды Института системного программирования РАН. Т. 29. 6. 2017, с. 25—48. doi: 10.15514/ISPRAS-2017-29(6)-2.
6. "Towards Automated Static Verification of GNU C Programs". Evgeny Novikov, Ilja Zakharov. Perspectives of System Informatics. Ed. By Alexander K. Petrenko and Andrei Voronkov. Cham: Springer International Publishing, 2018, pp. 402–416.
7. "A Survey of High-Performance Computing for Software Verification". Ilja Zakharov. Tools and Methods of Program Analysis. Ed. by Vladimir Itsykson, Andre Scedrov, and Victor Zakharov. Cham: Springer International Publishing, 2018, pp. 196–208.
8. "Pattern-based environment modeling for static verification of Linux kernel modules". I.S. Zakharov, V.S. Mutilin, A.V. Khoroshilov. Programming and Computer Software 41.3 (May 2015), pp. 183–195. doi: 10 . 1134 / S036176881503007X.