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

Верификацией называется процесс проверки соответствия программы требованиям (выяснения, является программа правильной или ошибочной). Данная книга посвящена важнейшему классу методов верификации — формальным методам и включает 16 лекций, сопровождаемых вопросами для самопроверки и упражнениями. В числе рассматриваемых тем: — обзор базовых методов верификации; — дедуктивный анализ программ; — проверка моделей; — использование формальных методов в тестировании. Издание будет полезно программистам, студентам и аспирантам, а также преподавателям и исследователям в области информатики и вычислительной техники. Ожидается, что читатель знает основы дискретной математики и математической логики.