name: Методы комплексного подхода к автоматизации дедуктивной верификации программ с финитными итерациями
keyword_list: семантическая разметка локализация ошибок стратегия доказательства аксиоматическая семантика финитная итерация спецификация дедуктивная верификация
abstract: Целью научной работы является разработка методов, обеспечивающих автоматизацию, расширяемость и проблемную ориентированность комплексного похода к формальной верификации программ без использования инвариантов циклов. Для достижения данной цели были поставлены следующие задачи: 
  1. Разработка метода, позволяющего генерировать условия корректности для программ с финитными итерациями без использования инвариантов циклов.
  2. Разработка стратегий, позволяющих автоматизировать доказательство условий корректности программ с финитными итерациями. Доказательство корректности данных стратегий.
  3. Разработка метода, позволяющего автоматизировать локализацию ошибок при дедуктивной верификации программ с финитными итерациями. 
  4. Разработка аксиоматической семантики языка Cloud Sisal, позволяющей проводить дедуктивную верификацию программ на данном языке без использования инвариантов циклических выражений. Разработка аксиоматической семантики расширения языка C конструкциями языка Sisal, позволяющей применять в системе CPPS методы комплексного подхода системы C-lightVer.
  5. Реализация методов комплексного подхода в системе C-lightVer, позволяющая при дедуктивной верификации программ с финитными итерациями, заданных на языках C, Cloud Sisal и на расширении C конструкциями Cloud Sisal, автоматизировать доказательство условий корректности и автоматизировать локализацию ошибок. Проведение экспериментов по автоматизированной верификации программ на данных языках.
  
  Положения, выносимые на защиту:
  1. Разработанный метод генерации операции замены для циклов позволяет генерировать условия корректности для программ с финитными итерациями без использования инвариантов циклов.
  2. Разработанные стратегии доказательства условий корректности позволяют автоматизировать проверку на истинность условий корректности программ с финитными итерациями.
  3. Разработанный метод локализации ошибок позволяет автоматизировать сопоставление конструкций программы и подформул условий корректности, а также локализацию ошибок в программах с финитными итерациями.
  4. Разработанная аксиоматическая семантика языка Cloud-Sisal-kernel позволяет проводить дедуктивную верификацию программ на этом языке без использования инвариантов циклических выражений. Разработанная аксиоматическая семантика расширения (C-Sisal-kernel) языка C конструкциями языка Sisal позволяет применять в системе CPPS методы комплексного подхода системы C-lightVer.
  5. Реализация методов комплексного подхода в системе C-lightVer позволила провести эксперименты по автоматизированной дедуктивной верификации программ с финитными итерациями на языках С, Cloud-Sisal-kernel и C-Sisal-kernel.
  
  Научная новизна работы состоит в:
  1. Автоматизации доказательства УК программ с финитными итерациями без использования инвариантов циклов.
  2. Автоматизации локализации ошибок при дедуктивной верификации программ с финитными итерациями без использования инвариантов циклов.
  3. Применимости разработанного комплексного подхода к программам с финитными итерациями на языках императивного программирования (на примере языка C), на языках функционального программирования (на примере языка Cloud Sisal) и на языках, основанных на обеих парадигмах программирования (на примере языка C-Sisal-kernel).
  
  Методология исследования базируется на подходах информатики к формальной верификации программ. В работе используется метод дедуктивной верификации программ, метод слабейшего предусловия, символический метод верификации финитных итераций, метод метагенерации условий корректности для упрощения расширения генератора УК, метод смешанной аксиоматической семантики для упрощения УК, стратегии автоматизации доказательства УК, метод семантической разметки для локализации ошибок.
  
  Цели и задачи исследования соответствуют следующим пунктам паспорта специальности 05.13.11: модели, методы и алгоритмы проектирования и анализа программ и программных систем, их эквивалентных преобразований,
  верификации и тестирования (пункт 1); языки программирования и системы программирования, семантика программ (пункт 2); программные системы символьных вычислений (пункт 5).
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: 50.05.19
rubrics.name: Теоретические основы прикладного программного обеспечения
rubrics.code: 50.05.09
rubrics.name: Языки программирования
rubrics.code: 50.05.03
rubrics.name: Общетеоретические вопросы программирования
oecds.code: 01.02.EX
oecds.name: COMPUTER SCIENCE, THEORY & METHODS
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: 1025403664340
author_organization.supervisor_name: АНДРЕЙ
author_organization.supervisor_surname: ПАЛЬЯНОВ
author_organization.supervisor_patronymic: ЮРЬЕВИЧ
author_organization.organization_type: Организация
author_organization.okogu: Министерство науки и высшего образования Российской Федерации
author_organization.okopf: Федеральные государственные бюджетные учреждения