Защита диссертации - Мандрыкин Михаил Усамович

Мандрыкин Михаил Усамович

Моделирование памяти Си-программ для инструментов статической верификации на основе SMT-решателей

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

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

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

Дата размещения: 2016-10-13.
Текст диссертации: Скачать

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

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

Место работы, должность: Федеральное государственное бюджетное учреждение науки Научно-исследовательский институт системных исследований Российской академии наук, заведующий сектором автоматизации программирования.

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

1. Галатенко В.А. К проблеме автоматизации анализа и обработки информационного наполнения безопасности. - "Программная инженерия", N 3, 2011. - С. 45-57.
2. Галатенко В.А. К автоматизации процессов анализа и обработки информационного наполнения безопасности: развитие протокола SCAP. - "Программная инженерия", N 4, 2012. - С. 9-13.
3. Аристов М.С., Галатенко В.А., Костюхин К.А., Шмырев Н.В. Использование свободно распространяемых средств статического анализа исходных текстов программ в процессе разработки приложений для операционных систем реального времени. - "Программная инженерия", N 5, 2012. - с. 2-6.
4. Галатенко В.А. Категорирование и разделение программ и данных как принцип архитектурной безопасности. - "Программная инженерия", N 7, 2012. - С. 2-7.
5. Вьюкова Н.И., Галатенко В.А., Костюхин К.А., Шмырев Н.В. Опыт использования адаптивной компиляции в целях оптимизации критически важных приложений. - "Программная инженерия", N 8, 2012. - с. 10-16.
6. Бетелин В.Б., Галатенко В.А., Костюхин К.А. Основные понятия контролируемого выполнения сложных систем. - "Информационные технологии. Приложение к журналу", N 3, 2013, 32 с.
7. Вьюкова Н.И., Галатенко В.А., Самборский С.В. LLVM как инфраструктура разработки компиляторов для встроенных систем. - "Программная инженерия", N 6, 2013. - с. 2-10.
8. Вьюкова Н.И., Галатенко В.А., Самборский С.В. О стандарте C11. - "Программная инженерия", N 8, 2013. - с. 2-9.
9. К вопросу по строения формальных моделей сбоеустойчивых приложений реального времени Галатенко В.А., Костюхин К.А., Шмырев Н.В. Интеллектуальные системы. Теория и приложения. 2013. Т. 17. № 1-4. С. 231-236.
10. К постановке задачи разграничения доступа в распределенной объектной среде. Галатенко А.В., Галатенко В.А. Программная инженерия. 2013. № 5. С. 27-30.
11. Модель памяти многопоточных программ в стандарте C11. Вьюкова Н.И., Галатенко В.А., Самборский С.В. Программная инженерия. 2013. № 10. С. 2-9.
12. Основные понятия контролируемого выполнения сложных систем. Бетелин В.Б., Галатенко В.А., Костюхин К.А. Информационные технологии. 2013. № S3. С. 1-32.
13. Controlled execution with explicit model. Бетелин В.Б., Галатенко В.А., Костюхин К. А. PROGRAMMING AND COMPUTER SOFTWARE, 2014, № 6, Т. 40, стр. 305 - 313
14. Трассировка и самолечение в POSIX-системах. Бомбин А.А., Галатенко В.А., Костюхин К.А. Программные продукты и системы, 2014, № 108, стр. 5 - 9
15. К вопросу самовосстановления программного обеспечения в ARINC- и POSIX-системах. Бомбин А.А., Галатенко В.А., Костюхин К.А. Программная инженерия, 2015, № 3, стр. 3 - 12

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

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

Место работы, должность: Федеральный исследовательский центр Институт прикладной математики им. М.В. Келдыша Российской академии наук, старший научный сотрудник.

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

1. Климов Ю.А. , Шворин А.Б., Хренов А.Ю., Адамович И.А., Орлов А.Ю., Абрамов С.М., Шевчук Ю.В., Пономарев А.Ю. Паутина: высокоскоростная коммуникационная сеть // Программные системы: теория и приложения: электронный научный журнал. — 2015. — Т. 6, № 1 (24). — С. 109-120.
2. Левин В. К., Четверушкин Б. Н., Елизаров Г. С., Горбунов В. С., Лацис А. О., Корнеев В. В., Соколов А. А., Андрюшин Д. В., Климов Ю. А. Коммуникационная сеть МВС-Экспресс // Информационные технологии и вычислительные системы. — 2014. — № 1. — С. 10-24.
3. Богословский Н.А., Климов Ю.А., Савельев А.В., Шалыга Д.К. Разработка экспериментального комплекса суперкомпьютерного моделирования на основе кода на языке Matlab // Программные системы: теория и приложения: электронный научный журнал. — 2013. — Т. 4, № 2 (16). — С. 21-42.
4. Елизаров Г.С., Горбунов В.С., Левин В.К., Лацис А.О., Корнеев В.В., Соколов А.А., Андрюшин Д.В., Климов Ю.А. Коммуникационная сеть МВС-Экспресс // Вычислительные методы и программирование. — 2012. — Т. 13 — Раздел 2. — С. 103-109.
5. Климов Ю.А., Орлов А.Ю., Шворин А.Б. Перспективные подходы к созданию масштабируемых приложений для суперкомпьютеров гибридной архитектуры // Информационные технологии и вычислительные системы. — 2012. — № 2. — С. 3-10.
6. Климов Ю.А., Орлов А.Ю., Шворин А.Б. Программный инструментарий для трафаретных вычислений на гибридных суперкомпьютерах // Программные системы: теория и приложения: электронный научный журнал. — 2012. — Т. 3, № 2 (11). — С. 23-49.
7. Климов Ю.А., Орлов А.Ю., Шворин А.Б. SkifCh: эффективный коммуникационный интерфейс // Вестник Южно-Уральского государственного университета. — 2011. — № 25 (242). — Серия «Математическое моделирование и программирование». — Выпуск 9. — Челябинск: Издательский центр ЮУрГУ, 2011. — С.98-106.

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

Ведущая организация: Федеральное государственное бюджетное образовательное учреждение высшего образования «Санкт- Петербургский государственный университет»

Контактные данные: 199034, Санкт-Петербург, Университетская наб. д.7/9, +7 (812) 328-97-01, spbu@spbu.ru, http://www.spbu.ru

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

1. Кознов Д.В., Ларчик Е.В., Терехов А.Н. ТРАНСФОРМАЦИЯ ДИНАМИЧЕСКИХ ПРЕДСТАВЛЕНИЙ В ПРЕДМЕТНО-ОРИЕНТИРОВАННОМ ВИЗУАЛЬНОМ МОДЕЛИРОВАНИИ. Программирование. 2015. № 4. С. 3-12.
2. Dmitry Boulytchev. Combinators and Type-Driven Transformers in Objective Caml. Science of Computer Programming, 2015
3. Daniil Berezun, Dmitry Boulytchev. Precise Garbage Collection for C++ with a Non-Cooperative Compiler Proceedings of the 10th Central and Eastern European Software Engineering Conference in Russia, 2014
4. Dmitry Boulytchev, Sergey Mechtaev. Efficiently Scrapping Boilerplate Code in OCaml. Workshop on ML, 2011
5. Anton Podkopaev, Dmitry Boulytchev. Polynomial-Time Optimal Pretty-Printing Combinators with Choice. Proceedings of 9th International Andrei Ershov Memorial Conference on Perspectives of System Informatics, 2014
6. Daniil Berezun, Dmitry Boulytchev. Precise Garbage Collection for C++ with a Non-Cooperative Compiler Proceedings of the 10th Central and Eastern European Software Engineering Conference in Russia, 2014
7. Koznov D.V., Luciv D.V., Basit H.A., Lieh O.E., Smirnov M.N. CLONE DETECTION IN REUSE OF SOFTWARE TECHNICAL DOCUMENTATION. Lecture Notes in Computer Science. 2016. Т. 9609. С. 170-185.
8. Кудрявцев Д.В., Кознов Д.В., Григорьев Л.Ю. СРЕДСТВА ТИПИЗАЦИИ И ПРАГМАТИКА ЯЗЫКА МОДЕЛИРОВАНИЯ ОРГ-МАСТЕР. Научно-технический вестник информационных технологий, механики и оптики. 2013. № 6 (88). С. 79-85.
9. Луцив Д.В., Кознов Д.В., Андреев В.С. ИЕРАРХИЧЕСКИЙ АЛГОРИТМ DIFF ПРИ РАБОТЕ СО СЛОЖНЫМИ ДОКУМЕНТАМИ. Системное программирование. 2012. Т. 7. № 1. С. 57-68.

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

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

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

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