Защита диссертации - Мордань Виталий Олегович

Мордань Виталий Олегович

Методы верификации программ на основе композиции задач достижимости

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

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

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

Дата размещения: 2017-03-23.
Текст диссертации: Скачать

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

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

Место работы, должность: Федеральное государственное бюджетное образовательное учреждение высшего образования «Ярославский государственный университет им. П.Г. Демидова», заведующий кафедрой теоретической информатики факультета информатики и вычислительной техники.

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

1. Kuzmin E.V., Ryabukhin D.A., Sokolov V.A. On the expressiveness of the approach to constructing PLC-programs by LTL-specification // Automatic Control and Computer Sciences, 50 (7), 2016. PP. 510-519. doi:10.3103/S0146411616070130.
2. S.V. Korsakov, A.V. Smirnov, V.A. Sokolov, Principles of Organizing the Interoperability of Equipollent Nodes in a Wireless Mesh-Network with Time Division Multiple Access. //Automatic Control and Computer Sciences. Allerton Press, Inc. 2016. V. 50, №6. PP. 415–422. ISSN 0146-4116.
3. Chaly D.Ju., Nikitin E.S., Antoshina E.Ju., Sokolov V.A. End-to-end Information Flow Security Model for Software-Defined Networks.// Моделирование и анализ информационных систем, 2015. Т. 22, № 6. С. 735-749. DOI: 10.18255/1818-1015-2015-6-735-749.
4. Соколов В.А., Корсаков С.В., Смирнов А.В., Башкин В.А., Никитин Е.С. Инструментальная система для поддержки разработки и исследования программно-конфигурируемых сетей подвижных объектов.// Моделирование и анализ информационных систем, 2015. Т. 22, № 4. С. 546-562. DOI: 10.18255/1818-1015-2015-4-546-562.
5. Кузьмин Е.В., Рябухин Д.А., Соколов В.А. О выразительности подхода к построению ПЛК-программ по LTL-спецификации // Моделирование и анализ информационных систем. 2015. Т. 22. №4. С. 507-520.
6. Kuzmin E.V., Sokolov V.A., Ryabukhin D.A. Construction and Verification of PLC-programs by LTL-specification // Automatic Control and Computer Sciences, 49 (7), 2015. PP. 453-465. doi: 10.3103/S0146411615070159
7. Kuzmin E.V., Sokolov V.A., Ryabukhin D.A. Construction and Verification of PLC LD-programs by LTL-specification // Automatic Control and Computer Sciences, 48 (7), 2014. PP. 424-436. doi: 10.3103/S014641161407013X
8. Kuzmin E.V., Ryabukhin D.A., Sokolov V.A. Modeling a Consistent Behavior of PLC-Sensors // Automatic Control and Computer Sciences, 48 (7), 2014. PP. 602-614. doi: 10.3103/S0146411614070256
9. Kuzmin E.V., Sokolov V.A. Modeling, Specification and Construction of PLC-programs // Automatic Control and Computer Sciences, 48 (7), 2014. PP. 554-563. doi: 10.3103/S0146411614070244
10. E. Boytsov, V. Sokolov. Comparison of Data Management Strategies for Multi-Tenant Database Cluster. // Proceedings of the Fourth International Symposium on Business Modelling and Software Design. SciTePress, Luxembourg, 2014. P. 217-222. http://www.is-bmsd.org/ Documents/ProceedingsOfFourthBMSD.pdf
11. Kuzmin E.V., Sokolov V.A. The Modeling of Counter Machines by Two-Head Finite Automata // Automatic Control and Computer Sciences, Vol.47, No.7, 2013, pp.541–544. http://link.springer.com/article/10.3103/S0146411613070122
12. Kuzmin E.V., Sokolov V.A. On Construction and Verification of PLC-Programs // Automatic Control and Computer Sciences, Vol.47, No.7, 2013, pp.443–451. http://link.springer.com/article/10.3103/S0146411613070110
13. E. Boytsov and V. Sokolov, The Development of an Imitation Model of a Multi-Tenant Database Cluster.// Proc. of the 3d International Symposium on Business Modeling and Software Design (BMSD-2013), Noordwijkerhout, The Netherlands, July 8-10, 2013. P. 237-244.
14. Evgeny Boytsov and Valery Sokolov, Multi-tenant Database Clusters for SaaS // Proceedings of the Second International Symposium on Business Modeling and Software Design BMSD-2012, Geneva, Switzerland, July 4-6, 2012. P. 144-149.

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

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

Место работы, должность: Публичное акционерное общество "Институт электронных управляющих машин им. И.С. Брука", начальник отделения «Системы программирования».

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

1. Волконский В.Ю, Брегер А.В., Бучнев А. Ю., Грабежной А.В., Ермолицкий А.В., Муханов Л.Е., Нейман-заде М.И., Степанов П.А., Четверина О.А. Методы распараллеливания программ в оптимизирующем компиляторе. //Вопросы радиоэлектроники, сер. ЭВТ, 2012, вып. 3. С.63-88.
2. Ермолицкий А.Е., Нейман-заде М.И., Четверина О.А., Маркин А.Л., Волконский В.Ю. Агрессивная инлайн-подстановка функций для VLIW-архитектур. // Труды ИСП РАН, Том 27, вып. 6, 2015 г.
3. Русяев Р.М., Нейман-заде М.И., Ермолицкий А.Е., Волконский В.Ю. Программно-аппаратные средства выявления ошибок обращения к памяти для архитектуры «Эльбрус». //Вопросы радиоэлектроники, сер. ЭВТ вып. 2, 2017, №3. С.33-38.
4. Ким А.К., Бычков И.Н., Волконский В.Ю., Воробушков В.В., Груздов Ф.А., Михайлов М.С., Парахин Ю.Н., Сахин Ю.Х., Семенихин С.В., Слесарев М.В., Фельдман В.М. Архитектурная линия "Эльбрус" сегодня: микропроцессоры, вычислительные комплексы и программное обеспечение. // Современные информационные технологии и ИТ-образование. Сборник докладов 7-й международной научно-практической конференции, Москва, 9-11 ноября 2012. С.21-29.
5. Ким А.К., Бычков И.Н., Волконский В.Ю., Воробушков В.В., Груздов Ф.А., Михайлов М.С., Нейман-заде М.И., Парахин Ю.Н., Семенихин С.В., Слесарев М.В., Фельдман В.М. Российские технологии "Эльбрус" для персональных компьютеров, серверов и суперкомпьютеров. // Современные информационные технологии и ИТ-образование. Сборник докладов 9-й международной научно-практической конференции, Москва, 14-16 ноября 2014. С.39-49.
6. Ким А.К., Волконский В.Ю., Груздов Ф.А., Нейман-заде М.И., Тихорский В.В. Аппаратно-программные технологии, реализованные на базе микропроцессоров с архитектурой «Эльбрус». // Качество и жизнь. Научно-производственный и культурно-образовательный ж-л Миннауки. Специальный выпуск. 2016. С.81-89.
7. Roman M. Rusiaev, Murad I. Neiman-Zade, Alexandr V. Ermolitsky, Valery I. Perekatov, and Vladimir Yu. Volkonsky. Various Buffer Overflow Detection Means for Elbrus Microprocessors. // IEEE Proceedins of the 2016 International Conference on Engineering and Telecommunication (EnT-2016). November 29, 2016. P.118-122.

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

Ведущая организация: Федеральный исследовательский центр "Информатика и управление" Российской Академии Наук

Контактные данные: 119333, Москва, Вавилова, д.44, кор.2, +7 499 1356260, ipiran@ipiran.ru, ipiran.ru

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

1. Nikolay A. Skvortsov, Leonid A. Kalinichenko, Dana A. Kovaleva, Oleg Y. Malkov. Search for hierarchical stellar systems of maximal multiplicity. Selected Papers of the XVII International Conference on Data Analytics and Management in Data Intensive Domains (DAMDID/RCDL 2015). CEUR Workshop Proceedings, ISSN 1613-0073, Vol. 1752. P. 219-225.
2. Sergey Stupnikov. Formal Semantics of a Language for Entity Resolution and Data Fusion and its Application for Verification of Data Integration Workflows. Selected Papers of the XVII International Conference on Data Analytics and Management in Data Intensive Domains (DAMDID/RCDL 2015). CEUR Workshop Proceedings, ISSN 1613-0073, Vol. 1752. P. 159-167.
3. Nikolay A. Skvortsov, Leonid A. Kalinichenko, Dmitry Yu. Kovalev. Conceptual modeling of subject domains in data intensive research. Selected Papers of the XVII International Conference on Data Analytics and Management in Data Intensive Domains (DAMDID/RCDL 2015). CEUR Workshop Proceedings, ISSN 1613-0073, Vol. 1752. P. 7-15.
4. N. A. Skvortsov, E. A. Avvakumova, D. O. Bryukhov, A. E. Vovchenko, A. A. Volnova, O. B. Dluzhnevskaya, P. V. Kaygorodov, L. A. Kalinichenko, A. Yu. Knyazev, D. A. Kovaleva, O. Yu. Malkov, A. S. Pozanenko, and S. A. Stupnikov. Conceptual Approach to Astronomical Problems. Astrophysical Bulletin. 71(1):114-124, 2016.
5. Stupnikov S. A., Briukhov D. O., Skvortsov N. A. Co-lending Systemic Risk Analysis over Heterogeneous Data Collections. Informatics and Applications. Moscow: IPI RAN, 2016. -- V. 10, Iss. 1. -- P. 24-34.
6. Stupnikov Sergey, Miloslavskaya Natalia, Budzko Vladimir. Unification of Graph Data Models for Heterogeneous Security Information Resources’ Integration. Proc. of the 3rd International Conference on Future Internet of Things and Cloud. IEEE, 2015. -- P. 457-464.
7. L. A. Kalinichenko, S. A. Stupnikov, A. E. Vovchenko, D. Y. Kovalev. Multi-Dialect Workflows. Advances in Databases and Information Systems: Proc. of the 18th East European Conference. LNCS 8716. -- Berlin-Heidelberg: Springer-Verlag, 2014. -- P. 352-365.
8. Kalinichenko L. A., Stupnikov S. A., Vovchenko E. A., Kovalev D. Y. Conceptual Declarative Problem Specification and Solving in Data Intensive Domains. Informatics and Applications. Moscow: IPI RAN, 2013. -- V. 7, Iss. 4. -- P. 112-139.
9. Kalinichenko L. A., Stupnikov S. A., Vovchenko E. A., Kovalev D. Y. Rule-based Multi-dialect Infrastructure for Conceptual Problem Solving over Heterogeneous Distributed Information Resources. New Trends in Databases and Information Systems. Selected Papers of the 17th European Conference on Advances in Databases and Information Systems and Associated Satellite Events. – Springer, 2013. Advances in Intelligent Systems and Computing, V. 241. – P. 61-68.

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

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

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

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