Защита диссертации - Захаров Илья Сергеевич

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

Методы декомпозиции систем и моделирования окружения программных модулей для верификации Си-программ

Диссертация защищена

Искомая степень: Кандидат физико-математических наук.

Специальность: 05.13.11 – Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей.

Дата размещения: 20 марта 2019.
Текст диссертации: Скачать

Решение совета о принятии диссертации к защите: Диссертация принята к защите.
Автореферат: Скачать
Отзыв научного руководителя: Скачать
Дата защиты: 23 мая 2019.

Официальный оппонент: Тормасов Александр Геннадьевич, доктор физико-математических наук (05.13.18).

Место работы, должность: Автономная некоммерческая организация высшего образования «Университет Иннополис», ректор.

Основные публикации за последние 5 лет:

1. Zykov S. V. et al. Applicative-based automatic configuration management for virtual machines //Procedia Computer Science. – 2018. – Т. 126. – С. 1771-1778.
2. Zykov S. V., Shumsky L. D., Tormasov A. G. Experimental design of automatic virtual machine configuration based on applicative approach //Procedia computer science. – 2017. – Т. 112. – С. 1721-1729.
3. Zykov S. V., Shumsky L. D., Tormasov A. G. Experimental design of automatic virtual machine configuration based on applicative approach //Procedia computer science. – 2017. – Т. 112. – С. 1721-1729.
4. Bykov A. et al. Towards Non-invasive Software Measurement System: Architecture and Implementation //International Conference in Software Engineering for Defence Applications. – Springer, Cham, 2016. – С. 149-165.
5. Pleshchinskii N., Tormasov A., Tumakov D. Analysis of the Fault Tolerance of the Distributed Data Storage with Controlled Redundancy //Applied Mathematical Sciences. – 2015. – Т. 9. – №. 141. – С. 7011-7025.
6. Маркеева Л. Б., Мелехова А. Л., Тормасов А. Г. Однородность виртуализационных событий, порожденных различными операционными системами //Труды Московского физико-технического института. – 2014. – Т. 6. – №. 3 (23).
7. Битнер В.А., Тормасов А.Г. Анализ и сокращение промежуточного представления программы в модели статического анализа нахождения состояния гонки в многопоточных алгоритмах // Вестник Казанского государственного технического университета им. А.Н. Туполева. – 2014. – № 3. – С. 172-177.

Отзыв оппонента: Скачать

Официальный оппонент: Буренков Владимир Сергеевич, кандидат технических наук (05.13.11).

Место работы, должность: АО «Лаборатория Касперского», разработчик-исследователь.

Основные публикации за последние 5 лет:

1. Буренков В. С., Иванов С. Р. Метод построения абстрактных моделей, используемых для верификации протоколов когерентности кэш-памяти масштабируемых систем //Вестник Московского государственного технического университета им. НЭ Баумана. Серия «Приборостроение». – 2017. – №. 1 (112).
2. Burenkov V. S. A technique for parameterized verification of cache coherence protocols //Труды Института системного программирования РАН. – 2017. – Т. 29. – №. 4.
3. Буренков В. С. О консервативном преобразовании формальных моделей, используемых применительно к масштабируемым системам для верификации протоколов когерентности памяти/Буренков ВС //Вопросы радиоэлектроники. – 2016. – №. 3. – С. 48-52.
4. Буренков В. С., Камкин А. С. Метод масштабируемой верификации PROMELA-моделей протоколов когерентности кэш-памяти //Проблемы разработки перспективных микро-и наноэлектронных систем (МЭС). – 2016. – №. 2. – С. 54-60.
5. Burenkov V. S., Kamkin A. S. Checking parameterized Promela models of cache coherence protocols //Труды Института системного программирования РАН. – 2016. – Т. 28. – №. 4.
6. Буренков В. С. Анализ применимости формальных методов к верификации протоколов когерентности кэш-памяти масштабируемых систем //Вопросы радиоэлектроники.– 2015. – №. 1. – С. 105-116.
7. Буренков В. С. Генератор тестов для верификации протокола когерентности кэшпамяти //Вопросы радиоэлектроники, серия ЭВТ. – 2014. – №. 3. – С. 56-63.

Отзыв оппонента: Скачать

Ведущая организация: Федеральное государственное учреждение «Федеральный исследовательский центр Институт прикладной математики им.М.В.Келдыша Российской академии наук».

Контактные данные: 125047, Москва, Миусская пл., д.4, +7(499)978-13-14, office@keldysh.ru, keldysh.ru

Основные публикации за последние 5 лет:

1. Grechanik S. A. Polyprograms and polyprogram bisimulation //Моделирование и анализ информационных систем. – 2018. – Т. 25. – №. 5. – С. 534-548.
2. Adamovich I. A., Klimov A. V. An interactive specializer based on partial evaluation for a Java subset //Труды института системного программирования РАН. – 2018. – Т. 30. – №. 4. – С. 29-44.
3. Климов А. В., Романенко С. А. Суперкомпиляция: основные принципы и базовые понятия //Препринты Института прикладной математики им. МВ Келдыша РАН. – 2018. – №. 0. – С. 111-36.
4. Романенко С. А. и др. Суперкомпиляция: гомеоморфное вложение, вызов по имени, частичные вычисления //Препринты ИПМ им. МВ Келдыша. – 2018. – №. 209. – С. 1-32.
5. Андреев, С. С., Дбар, С. А., Климов, Ю. А., Лацис, А. О., Плоткина, Е. А. Квантовая модель вычислений глазами классического программиста // Препринт ИПМ № 178, Москва, 2018, 30 с.
6. Дбар С.А., Лацис А.О. О МОДЕЛИ ПРОГРАММИРОВАНИЯ ВЫЧИСЛИТЕЛЬНОЙ СХЕМОТЕХНИКИ // В сборнике: Языки программирования и компиляторы - 2017 Труды конференции. Редактор: Д.В. Дубров. 2017. С. 98-100.
7. Гречаник С. А. Полипрограммы как представление множеств функциональных программ и преобразования над ними //Препринты Института прикладной математики им. МВ Келдыша РАН. – 2017. – №. 0. – С. 5-31.
8. Бондаренко А. А., Якобовский М. В. Моделирование отказов в высокопроизводительных вычислительных системах в рамках стандарта mpi и его расширения ulfm,Вестник Южно-Уральского государственного университета // Вестник Южно-Уральского государственного университета. Серия "Вычислительная математика и информатика". — 2015. — Т. 4, № 3. — С. 5–12.
9. Klyuchnikov I., Romanenko S. Certifying supercompilation for Martin-Löf’s type theory //International Andrei Ershov Memorial Conference on Perspectives of System Informatics.– Springer, Berlin, Heidelberg, 2014. – С. 186-200.
10. Левин, В.К., Четверушкин, Б.Н., Елизаров, Г.С., Горбунов, В.С., Лацис, А.О., Корнеев, В.В., Соколов, А.А., Андрюшин, Д.В. and Климов, Ю.А. Коммуникационная сеть МВС-Экспресс. // Информационные технологии и вычислительные системы. – 2014 – № 1 – C. 10-24.

Отзыв ведущей организации: Скачать

Решение диссертационного совета по результатам защиты диссертации: Принято решение о присуждении степени.

Присутствовало 15 из 22 членов диссертационного совета: Аветисян А.И., Томилин А.Н., Петренко А.К., Зеленов С.В., Белеванцев А.А., Бурдонов И.Б., Дроздов А.Ю., Евтушенко Н.В., Захаров В.Н., Крюков В.А., Кузнецов С.Д., Лаврищева Е.М., Семенов В.А., Серебряков В.А., Шнитман В.З.

Заключение диссертационного совета: Скачать