• A
  • A
  • A
  • АБВ
  • АБВ
  • АБВ
  • А
  • А
  • А
  • А
  • А
Обычная версия сайта
ФИО студента
Название работы
Руководитель
Факультет
Программа
Оценка
Год защиты
Путро Павел Андреевич
Метод дедуктивной верификации машинного кода без циклов
2018
При разработке программ на языках высокого уровня, разработчикам приходится делать предположение о корректности компилятора. Однако это может быть неприемлемо для критически важных систем. Поскольку на данный момент не существует полноценных компиляторов, для которых корректность доказана, автор предлагает решать эту проблему путём доказательства корректности сгенерированного машинного кода методами дедуктивной верификации. Для решения данной цели необходимо решить ряд задач, одной из которых является слияние модели спецификаций пред- и постусловий с моделью поведения машинного кода. В отчёте представлено экспериментальное исследование с целью построения инструмента доказательства корректности машинного кода Си функций без циклов, с использованием дедуктивной верификации и SMT-решателей. В результате такой инструмент может быть использован для верификации машинного кода реальных критических систем, написанных на Си и аннотированных языком ACSL.

Научная новизна работы заключается в применении, разработанного автором, метода слияния спецификаций языка высокого уровня с моделью поведения машинного кода, а также использовании языка описания архитектуры микропроцессоров для спецификации модели целевого процессора.

Работа содержит 62 страницы, 3 главы, 50 рисунков, 33 источника.

Ключевые слова: машинный код, дедуктивная верификация, формальная спецификация, ACSL, SMT-решатели, Frama-C, Why3.

Выпускные квалификационные работы (ВКР) в НИУ ВШЭ выполняют все студенты в соответствии с университетским Положением и Правилами, определенными каждой образовательной программой.

Аннотации всех ВКР в обязательном порядке публикуются в свободном доступе на корпоративном портале НИУ ВШЭ.

Полный текст ВКР размещается в свободном доступе на портале НИУ ВШЭ только при наличии согласия студента – автора (правообладателя) работы либо, в случае выполнения работы коллективом студентов, при наличии согласия всех соавторов (правообладателей) работы. ВКР после размещения на портале НИУ ВШЭ приобретает статус электронной публикации.

ВКР являются объектами авторских прав, на их использование распространяются ограничения, предусмотренные законодательством Российской Федерации об интеллектуальной собственности.

В случае использования ВКР, в том числе путем цитирования, указание имени автора и источника заимствования обязательно.

Расширенный поиск ВКР