Гладштейн02дек25
Докладчик: Владимир Гладштейн (National University of Singapore) Тема: Loom - платформа для разработки Фундаментальных Мульти-Модальных Систем Верификации, часть 2: Veil Аннотация: В этом докладе мы продолжим говорить про Loom и затронем два новых аспекта которые не были освещены в первом докладе. Во-первых, я представлю Veil — платформу для автоматической и интерактивной верификации систем переходов (transition systems), специализиранный на построении машинных доказательств о конкурентных и распределённых алгоритмах. Veil как и Velvet построен на основе Loom. Он позволяет описывать системы переходов и их спецификации на простом императивном языке, тестировать ее, и затем, генерируя условия верификации (verification conditions) в логике первого порядка, автоматически доказывать ее корректность с помощью SMT-решателей. Точно так же как и в Velvet, eсли автоматическая верификация не справляется или если описание системы требует утверждений в логике высшего порядка, Veil предоставляет интерактивный режим верификации — благодаря тому, что он встроен в универсальный ассистент доказательств. Во-вторых мы вернемся к Velvet и посмотрим как в нем можно сочитать различные методы проверки корректности программ: property-based testing, доказательства тотальной и частичной корректности, а также доказательства корректности и некорректности.
Докладчик: Владимир Гладштейн (National University of Singapore) Тема: Loom - платформа для разработки Фундаментальных Мульти-Модальных Систем Верификации, часть 2: Veil Аннотация: В этом докладе мы продолжим говорить про Loom и затронем два новых аспекта которые не были освещены в первом докладе. Во-первых, я представлю Veil — платформу для автоматической и интерактивной верификации систем переходов (transition systems), специализиранный на построении машинных доказательств о конкурентных и распределённых алгоритмах. Veil как и Velvet построен на основе Loom. Он позволяет описывать системы переходов и их спецификации на простом императивном языке, тестировать ее, и затем, генерируя условия верификации (verification conditions) в логике первого порядка, автоматически доказывать ее корректность с помощью SMT-решателей. Точно так же как и в Velvet, eсли автоматическая верификация не справляется или если описание системы требует утверждений в логике высшего порядка, Veil предоставляет интерактивный режим верификации — благодаря тому, что он встроен в универсальный ассистент доказательств. Во-вторых мы вернемся к Velvet и посмотрим как в нем можно сочитать различные методы проверки корректности программ: property-based testing, доказательства тотальной и частичной корректности, а также доказательства корректности и некорректности.