Вступ до формальних методів верифікації програм. Олександр Камкін

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

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