Метод дедуктивной верификации машинного кода без циклов

При разработке программ на языках высокого уровня, разработчикам приходится делать предположение о корректности компилятора. Однако это может быть неприемлемо для критически важных систем. Поскольку на данный момент не существует полноценных компиляторов, для которых корректность доказана, автор предлагает решать эту проблему путём доказательства корректности сгенерированного машинного кода методами дедуктивной верификации. Для решения данной цели необходимо решить ряд задач, одной из которых является слияние модели спецификаций пред- и постусловий с моделью поведения машинного кода. В отчёте представлено экспериментальное исследование с целью построения инструмента доказательства корректности машинного кода Си функций без циклов, с использованием дедуктивной верификации и SMT-решателей. В результате такой инструмент может быть использован для верификации машинного кода реальных критических систем, написанных на Си и аннотированных языком ACSL. Научная новизна работы заключается в применении, разработанного автором, метода слияния спецификаций языка высокого уровня с моделью поведения машинного кода, а также использовании языка описания архитектуры микропроцессоров для спецификации модели целевого процессора. Работа содержит 62 страницы, 3 главы, 50 рисунков, 33 источника. Ключевые слова: машинный код, дедуктивная верификация, формальная спецификация, ACSL, SMT-решатели, Frama-C, Why3.