name: Логический язык программирования как инструмент спецификации и верификации динамической памяти
keyword_list: логический язык верификация спецификация динамическая память
abstract: Ошибки использования динамической памяти являются одними из самых дорогостоящих при разработке программного обеспечения на протяжении уже нескольких десятилетий. Локализация таких ошибок является трудной задачей, поскольку, довольно часто, видимое проявление некорректного поведения программы и реальный участок исходного кода его вызвавшего отстоят далеко друг от друга. Следовательно, разработка подходов и методов, упрощающих поиск и предотвращение ситуаций некорректного использования динамической памяти является актуальной задачей.
  Выразимость утверждений, полнота правил, и автоматизация в большой степени определяют успех верификации динамической памяти. Выразимость утверждений касается формализма утверждений и правил верификации. В существующей на текущий момент практике, описания динамической памяти сложны и часто неинтуитивны. Возможности логического вывода зачастую ограничиваются корректностью и полнотой правил верификации и представляют собой лишь «островные реализации», которые нельзя использовать на практике. Из-за большого количества соглашений(конвенций) в языках спецификации и верификации возможности верификации динамической
  памяти сильно ограничены. Верификация часто осуществляется нетривиально, объяснения принятия или отказа доказательства, как правило, контр-интуитивны.
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: 0
chairman_dissertation_council.scopus_author_id: 56785609900
chairman_dissertation_council.rinc_id: 2900
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: Прикладное программное обеспечение
oecds.code: 01.02.ET
oecds.name: COMPUTER SCIENCE, INFORMATION SYSTEMS
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: 1027806875381
protection_organization.organization_type: Организация
protection_organization.okogu: Министерство науки и высшего образования Российской Федерации
protection_organization.okopf: Федеральные государственные автономные учреждения
author_organization.short_name: СПбГЭТУ "ЛЭТИ"
author_organization.name: Федеральное государственное автономное образовательное учреждение высшего образования "Санкт-Петербургский государственный электротехнический университет “ЛЭТИ” им. В.И. Ульянова (Ленина)"
author_organization.ogrn: 1027806875381
author_organization.organization_type: Организация
author_organization.okogu: Министерство науки и высшего образования Российской Федерации
author_organization.okopf: Федеральные государственные автономные учреждения