Практическая важность техники верификации на модели обусловлена возрастающими требованиями к надежности и скорости разработки коммуникационных протоколов и интегральных схем, а также их возрастающей сложностью.
В докладе представлен общий подход к постановке задачи верификации на модели и ряд приложений. Будут затронуты следующие темы:
1. OBDD и их применение в model checking,
2. автоматы на бесконечных строках,
3. алгоритмы верификации на модели заданной формулами.