name: Автоматический вывод реляционных инвариантов для нелинейных систем дизъюнктов Хорна с ограничениями
keyword_list: ЛОГИКА ХОАРА ИНДУКТИВНЫЕ ИНВАРИАНТЫ ЛОГИКА ПЕРВОГО ПОРЯДКА ДИЗЪЮНКТЫ ХОРНА C ОГРАНИЧЕНИЯМИ ФОРМАЛЬНАЯ ВЕРИФИКАЦИЯ
abstract: В диссертации приводится частичное решение проблемы представимости символьных моделей нелинейных систем дизъюнктов Хорна с ограничениями: языки ограничений либо алгоритмически неразрешимы, либо недостаточно выразительны для представления решений некоторых систем дизъюнктов Хорна. Предложен метод синтаксической синхронизации дизъюнктов, доказана его корректность. Введён новый класс решений систем дизъюнктов, называемый реляционными сертификатами выполнимости, и показано, что этот вид решений строго более выразительный для представления решений нелинейных систем, чем классические символьные модели. Разработан алгоритм автоматического вывода реляционных сертификатов выполнимости. Проведено экспериментальное исследование, показывающее, что разработанный алгоритм успешно решает нелинейные системы.
   
  Диссертация выполнена в ФГБОУ ВО «Санкт-Петербургский государственный университет» на кафедре системного программирования.
  Научный руководитель – Кознов Дмитрий Владимирович, доктор технических наук, доцент, профессор кафедры системного программирования ФГБОУ ВО «Санкт-Петербургский государственный университет».
  
  Официальные оппоненты: 
  - Ломазова Ирина Александровна – доктор физико-математических наук, профессор, ФГАОУ ВО Национальный исследовательский университет высшей школы экономики, факультет компьютерных наук, департамент программной инженерии, профессор.
  - Шилов Николай Вячеславович – кандидат физико-математических наук, доцент, АНО ВО «Университет Иннополис», начальник лаборатории программной инженерии.
  
  Ведущая организация – ФГБУН Институт системного программирования Российской академии наук им. В.П.Иванникова  (ИСП РАН), Москва.
  
  Основные публикации:
  1.Мордвинов, Д.А. Направляемый свойством поиск реляционных инвариантов // Моделирование и анализ информационных систем. — 2019. — Т. 26, №. 4. — С. 550-571.
  2. Мордвинов Д.А. Автоматическое доказательство корректности программ с динамической памятью / Ю.О.Костюков, К.А.Батоев, Д.А.Мордвинов, М.П.Костицын, А.В.Мисонижник //Труды Института системного программирования РАН. – 2019.- Т. 31, № 5. – С. 37-62.
  3. Mordvinov, D. Property Directed Inference of Relational Invariants. / D. Mordvinov, G. Fedyukovich //Proceedings of the 19th Conference on Formal Methods in Computer-Aided Design (FMCAD 2019). – IEEE. — 2019. — P. 152-160.
chairman_dissertation_council.name: Александр
chairman_dissertation_council.surname: Марчук
chairman_dissertation_council.patronymic: Гурьевич
chairman_dissertation_council.position: главный научный сотрудник
chairman_dissertation_council.degree: Доктор физико-математических наук
chairman_dissertation_council.rank: Профессор
chairman_dissertation_council.wos_research_id: U-8105-2017
chairman_dissertation_council.scopus_author_id: 7006342715
chairman_dissertation_council.rinc_id: 2370
chairman_dissertation_council.url: http://marchuk.iis.nsk.su/
chairman_dissertation_council.orcid: 0000-0001-8455-725X
chairman_dissertation_council.territory: РОССИЯ
organization_supervisor.name: Андрей
organization_supervisor.surname: Пальянов
organization_supervisor.patronymic: Юрьевич
organization_supervisor.position: Директор
organization_supervisor.territory: РОССИЯ
rubrics.code: 50.41.25
rubrics.name: Прикладное программное обеспечение
rubrics.code: 27.03.19
rubrics.name: Математическая логика
rubrics.code: 27.03.55
rubrics.name: Теория доказательств
rubrics.code: 50.05.19
rubrics.name: Теоретические основы прикладного программного обеспечения
oecds.code: 01.02.00
oecds.name: Computer and information sciences
speciality_codes.name: Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей
speciality_codes.code: 05.13.11
supervisors.fio: Кознов Д.В.
supervisors.scientific_degree: Доктор технических наук
supervisors.speciality_code: Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей
supervisors.responsible_type: Научный руководитель
opponents.fio: Ломазова И.А.
opponents.scientific_degree: Доктор физико-математических наук
opponents.speciality_code: Теоретические основы информатики
opponents.responsible_type: Оппонент
opponents.fio: Шилов Н.В.
opponents.scientific_degree: Кандидат физико-математических наук
opponents.speciality_code: Математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей
opponents.responsible_type: Оппонент
protection_organization.short_name: ИСИ СО РАН
protection_organization.name: ФЕДЕРАЛЬНОЕ ГОСУДАРСТВЕННОЕ БЮДЖЕТНОЕ УЧРЕЖДЕНИЕ НАУКИ ИНСТИТУТ СИСТЕМ ИНФОРМАТИКИ ИМ. А.П. ЕРШОВА СИБИРСКОГО ОТДЕЛЕНИЯ РОССИЙСКОЙ АКАДЕМИИ НАУК
protection_organization.ogrn: 1025403664340
protection_organization.supervisor_name: АНДРЕЙ
protection_organization.supervisor_surname: ПАЛЬЯНОВ
protection_organization.supervisor_patronymic: ЮРЬЕВИЧ
protection_organization.organization_type: Организация
protection_organization.okogu: Министерство науки и высшего образования Российской Федерации
protection_organization.okopf: Федеральные государственные бюджетные учреждения
author_organization.short_name: Санкт-Петербургский государственный университет, Санкт-Петербургский университет, СПбГУ
author_organization.name: федеральное государственное бюджетное образовательное учреждение высшего образования "Санкт-Петербургский государственный университет"
author_organization.ogrn: 1037800006089
author_organization.organization_type: Организация
author_organization.okogu: Правительство Российской Федерации
author_organization.okopf: Федеральные государственные бюджетные учреждения