Kurin25nov25

Докладчик: Виталий Курин (Neapolis University Pafos) Тема: Loom: Платформа для разработки Фундаментальных Мульти-Модальных Систем Верификации Аннотация: Мульти-Модальная верификация программ — это процесс проверки соответствия кода его спецификации с использованием как динамических, так и символических методов, а также доказательства его корректности с помощью сочетания автоматических и интерактивных инструментов машинной поддержки. Чтобы таким инструментам можно было доверять, они сами должны сопровождаться формальными доказательствами корректности (soundness), устанавливающими, что любая программа, проверенная ими на соответствие спецификации, не нарушит её условия при исполнении. Инструменты верификации, корректность которых доказана внутри универсального доказательного ассистента с малым доверенным ядром, обычно называются фундаментальными (foundational). В этом докладе я представлю Loom: платформу, которая упрощает и оптимизирует разработку систем верификации программ, являющихся как Фундаментальными, так и Мульти-Модальными. Наш подход основан на известной идее Монадического Неглубоко Вложения (Monadic Shallow Embedding) семантики исполняемой программы в язык теорем прувера, основанного на логике высшего порядка, в нашем случае — Lean. Мы предоставляем библиотеку Трансформеров Монад (Monad Transformers) для такой семантики, кодирующую различные вычислительные эффекты, включая состояние, расходимость программ, обработка исключений и недетерминизм, а также механизм...