Введение в формальные методы верификации программ: Учебное пособие.

Авторы

А. С. Камкин

Аннотация

Книга является учебным пособием по формальным методам верификации программ и основана на курсах лекций, читаемых автором на факультете ВМК МГУ имени М. В. Ломоносова, ФУПМ МФТИ и ФКН ВШЭ. В ней изложены основы таких подходов, как дедуктивный анализ и проверка моделей. Список тем включает: методы формализации семантики языков программирования (операционная и аксиоматическая семантика), методы формальной спецификации требований (программные контракты и темпоральная логика линейного времени), методы доказательства корректности программ (метод индуктивных утверждений и метод фундированных множеств) и методы проверки моделей (теоретико-автоматный подход в явной и символической формах). В пособии также затрагиваются вопросы абстрактной интерпретации, разрешения ограничений, применения формальных методов в тестировании; даются сведения об инструментах Frama-C и Spin. Каждая глава сопровождается примерами и упражнениями. Пособие предназначено для студентов и аспирантов программистских специальностей, а также преподавателей и исследователей в области информатики и программной инженерии.

Ключевые слова

формальная спецификация, формальная верификация, дедуктивный анализ, проверка моделей, тестирование на основе моделей, Frama-C, Spin.

Издание

Москва: МАКС Пресс, 2018. – 272 с.

978-5-317-05767-1

Научная группа

Технологии программирования

Все публикации за 2018 год

Все публикации