Семинар «Mультимодальная верификация распределенных протоколов на Lean»

Selfmade

Новый семинар состоится 21 ноября 2025 онлайн. Ссылка на трансляцию будет вывешена здесь незадолго до старта.

Тема: «Mультимодальная верификация распределенных протоколов на Lean».

Докладчик: Владимир Гладштейн, аспирант в National Univeristy of Singapore, младший научный сотрудник в Amazon Web Services.

Аннотация: В докладе будет представлен Veil — платформа для автоматической и интерактивной верификации систем переходов (transition systems) со специализацией на построении машинных доказательств о конкурентных и распределённых алгоритмах. Veil реализован поверх ассистента доказательств Lean. Он позволяет описывать систему переходов и её спецификацию на простом императивном языке, тестировать ее, и затем, генерируя условия верификации (verification conditions) в логике первого порядка, автоматически доказывать ее корректность с помощью SMT-решателей.

Если автоматическая верификация не справляется или если описание системы требует утверждений в логике высшего порядка, Veil предоставляет интерактивный режим верификации — благодаря тому, что он встроен в универсальный ассистент доказательств. Производительность автоматической верификации в Veil достаточна для практических задач, при этом платформа поддерживает бесшовное совмещение автоматических и интерактивных доказательств спецификаций систем, выходящих за пределы возможностей существующих автоматических систем проверки корректности.

🗓 Дата: 21 ноября 2025

⏰ Время: 18:30

📍 Место: онлайн