Верификация — это проверка того, что аппаратная или программная система соответствует заявленной спецификации (то есть обладает необходимыми свойствами).

Данный курс является введением в методы верификации аппаратных и программных систем. В частности, будут освещены следующие темы:

• реактивные системы и их моделирование; временные логики;
• метод проверки моделей (model checking) и алгоритмы для проверки моделей;
• задача булевой выполнимости и ее роль в верификации аппаратных и программных систем.

Наряду с теоретическими основами верификации будут рассмотрены программные средства для верификации и примеры.