В рамках семинара слушатели получат первоначальный практический опыт непосредственной работы с системой верификации SPIN, возможности и средства проверки корректности программ с помощью SPIN. Будет рассказано об особенностях установки и запуска системы SPIN на компьютерах слушателей, будут рассмотрены режимы работы системы, решены задачи с обнаружением тонких ошибок в параллельных программах и протоколах. Будут рассмотрены примеры использования системы SPIN и метода верификации Model checking не только для верификации параллельных программ, но и для решения логических задач, выявления атаки в криптографическом протоколе аутентификации Нидхема-Шредера и т.п.