Камкин А.С. Введение в формальные методы верификации программ

М.: МАКС Пресс, 2018. — 272 с. — ISBN: 978-5-317-05767-1.Книга является учебным пособием по формальным методам верификации программ и основана на курсах лекций, читаемых автором на факультете ВМК МГУ имени М. В. Ломоносова, ФУПМ МФТИ и ФКН ВШЭ. В ней изложены основы таких подходов, как дедуктивный анализ и проверка моделей. Список тем включает: методы формализации семантики языков программирования (операционная и аксиоматическая семантика), методы формальной спецификации требований (программные контракты и темпоральная логика линейного времени), методы доказательства корректности программ (метод индуктивных утверждений и метод фундированных множеств) и методы проверки моделей (теоретико-автоматный подход в явной и символической формах). В пособии также затрагиваются вопросы абстрактной интерпретации, разрешения ограничений, применения формальных методов в тестировании; даются сведения об инструментах Frama-C и Spin . Каждая глава сопровождается примерами и упражнениями.
Пособие предназначено для студентов и аспирантов программистских специальностей, а также преподавателей и исследователей в области информатики и программной инженерии.Предисловие
Введение в формальные методы верификации программ.
Формализация семантики языков программирования.
Дедуктивная верификация последовательных программ.
Инструменты дедуктивной верификации программ.
Метод индуктивных утверждений.
Метод фундированных множеств.
Автоматический синтез инвариантов циклов.
Автоматическое доказательство условий верификации.
Спецификация и верификация параллельных программ.
Инструменты проверки моделей.
Моделирование программ структурами Крипке.
Автоматы Бюхи и ω-регулярные языки.
Синтез автомата Бюхи по формуле LTL.
Символическая проверка моделей.
Использование формальных методов в тестировании.
Используемые сокращения и обозначения.
Список источников.