Во вторник 2 декабря 2025 г. пройдет семинар "Теоретическое и экспериментальное программирование" (Руководитель: к.ф.-м.н., с.н.с. Гаранина Н.О., соруководители: к.ф.-м.н., н.с. Кондратьев Д.А., к.ф.-м.н., с.н.с. Ануреев И.С., секретарь: к.ф.-м.н. Шилов Н.В.).
Время проведения: 17.00-18.30 НСК (13.00-14.30 МСК) очно в к. 239 ИСИ СО РАН и онлайн по ссылке.
Анонсы, слайды докладов и другая информация будут доступны в группе телеграм.
Докладчик: Владимир Гладштейн (National University of Singapore, Amazon Web Services)
Тема: Loom: Платформа для разработки Фундаментальных Мульти-Модальных Систем Верификации, часть 2
В этом докладе мы продолжим говорить про Loom и затронем два новых аспекта которые не были освещены в первом докладе. Во-первых, я представлю Veil — платформу для автоматической и интерактивной верификации систем переходов (transition systems), специализиранный на построении машинных доказательств о конкурентных и распределённых алгоритмах. Veil как и Velvet построен на основе Loom. Он позволяет описывать системы переходов и их спецификации на простом императивном языке, тестировать ее, и затем, генерируя условия верификации (verification conditions) в логике первого порядка, автоматически доказывать ее корректность с помощью SMT-решателей. Точно так же как и в Velvet, eсли автоматическая верификация не справляется или если описание системы требует утверждений в логике высшего порядка, Veil предоставляет интерактивный режим верификации — благодаря тому, что он встроен в универсальный ассистент доказательств.
Во-вторых мы вернемся к Velvet и посмотрим как в нем можно сочитать различные методы проверки корректности программ: property-based testing, доказательства тотальной и частичной корректности, а также доказательства корректности и некорректности.
Слайды будут на английском, выступление - на русском.