Семинар теоретического и экспериментального программирования имени В.А. Непомнящего

Это обзорный доклад, фокусирующийся на алгоритмах сортировки и поиска ближайших соседей в многомерных векторных пространствах — ключевых операциях векторных СУБД. Дается краткое описание роли векторных СУБД как важных компонентов автономных больших языковых моделей (agentic LLMs). Анализируется проблема “проклятия размерности”, которая является непреодолимым препятствием на пути к точному решению задачи поиска ближайших соседей. Классифицируются основные подходы к решению приближенного варианта данной задачи и методы их сравнения друг с другом. Также рассматривается роль современных аппаратных средств в ускорении работы с многомерными векторными данными на примере некоторых конкретных подходов. Доклад завершается формулировкой острых проблем, стоящих перед разработчиками и пользователями прикладных векторных СУБД, а также кратким обзором оригинальных подходов к решению этих проблем.

Baldur — это экспериментальная система автоматизированного доказательства теорем, которая использует большие языковые модели (LLM) для решения задач формальной верификации программ. LLM в Baldur генерирует шаги доказательства, леммы и инварианты, а также предлагает возможные направления доказательства, после чего все сгенерированные элементы проверяются традиционными системами машинной поддержки доказательства. Такой гибридный подход обеспечивает высокую степень автоматизации при сохранении формальной корректности. Baldur эффективно решает задачи анализа безопасности, проверки свойств исполнения и доказательства функциональной корректности программ. Система ориентирована на совместную работу эксперта и модели, обеспечивая прозрачность, трассируемость и воспроизводимость рассуждений. Благодаря использованию больших языковых моделей Baldur ускоряет разработку доверенного программного обеспечения и расширяет возможности автоматического синтеза доказательств.

Большое пространство состояний реальных программ затрудняет или делает невозможной их непосредственную верификацию методом проверки модели (model checking). Наличие симметрии в программе достаточно часто позволяет упростить модель и сократить её пространство состояний, что приводит к резкому снижению времени верификации. Классический подход состоит в обнаружении группы симметрии и построении на её основе упрощенной модели для верификации. Однако не все инструменты имеют поддержку симметрии, а инструменты с такой поддержкой не всегда справляются с поставленной задачей.

В докладе предлагается альтернативный классическому подход к разработке программ основанный на симметрии. В программе выделяется ядро – координационный центр, который работает с учётом симметрии и отвечает за выполнимость заданных темпоральных свойств.

Ядро координирует вычисления, которые вынесены за его пределы – в обвязку ядра. В связи с этим ядро имеет небольшое пространство состояний и может быть верифицировано методом проверки модели. Обвязка не может вмешиваться в работу верифицированного ядра и нарушать его свойства.

Подход продемонстрирован на примере разработки и верификации арбитра ресурсов марсохода. Арбитр координирует доступ n процессов к m ресурсам, где n и m -- натуральные числа. Используются язык программирования C/C++ и инструмент проверки модели Spin. Модель поведения ядра автоматически извлекается верификатором Spin из C-кода. Проверке подлежат темпоральные свойства, выраженные в логике LTL.

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

Во-вторых мы вернемся к Velvet и посмотрим как в нем можно сочитать различные методы проверки корректности программ: property-based testing, доказательства тотальной и частичной корректности, а также доказательства корректности и некорректности.

Слайды будут на английском, выступление - на русском.

Мульти-Модальная верификация программ — это процесс проверки соответствия кода его спецификации с использованием как динамических, так и символических методов, а также доказательства его корректности с помощью сочетания автоматических и интерактивных инструментов машинной поддержки. Чтобы таким инструментам можно было доверять, они сами должны сопровождаться формальными доказательствами корректности (soundness), устанавливающими, что любая программа, проверенная ими на соответствие спецификации, не нарушит её условия при исполнении. Инструменты верификации, корректность которых доказана внутри универсального доказательного ассистента с малым доверенным ядром, обычно называются фундаментальными (foundational).

В этом докладе я представлю Loom: платформу, которая упрощает и оптимизирует разработку систем верификации программ, являющихся как Фундаментальными, так и Мульти-Модальными. Наш подход основан на известной идее Монадического Неглубоко Вложения (Monadic Shallow Embedding) семантики исполняемой программы в язык теорем прувера, основанного на логике высшего порядка, в нашем случае — Lean. Мы предоставляем библиотеку Трансформеров Монад (Monad Transformers) для такой семантики, кодирующую различные вычислительные эффекты, включая состояние, расходимость программ, обработка исключений и недетерминизм, а также механизм автоматического вывода соответствующих генераторов корректных условий верификации.

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

Одна из систем верификации, основанная на Loom - язык Velvet. Пользователи могут использовать Velvet для спецификации императивных программ в стиле Dafny и их механической верификации. В рамках соревнования VeHa 2025 язык Velvet получилось успешно применить для задачи верификации алгоритма поиска подстроки.

Слайды будут на английском, выступление - на русском.

Представляется подход к дедуктивному синтезу программ с использованием секвенциального метода Генцена в рамках логического программирования. Используя секвенциальное исчисление как формальную систему для структурированного логического вывода, наш метод автоматизирует вывод доказуемо корректных программ из спецификаций, выраженных в логике предикатов первого порядка без отрицаний. Мы формализуем синтаксис и семантику секвенциального исчисления, реализуя его основные правила вывода (правила введения и удаления) в логическом программировании для обеспечения масштабируемого синтеза. Практические примеры демонстрируют преобразование логических спецификаций в исполняемые программы. Подход обеспечивает формальную корректность через конструктивную семантику реализуемости Клини, при этом синтезированные программы работают в субрекурсивном языке, чтобы гарантировать завершение вычислительных процессов. Мы оцениваем сильные стороны метода, включая его надежность для систем с критической безопасностью, и его ограничения, такие как вычислительная сложность для неограниченных конструкций. В сравнении с синтезом, управляемым ИИ, наш подход ставит на первое место формальные гарантии, дополняя современные тенденции. Направления будущих исследований включают оптимизацию вычислительной эффективности и расширение применимости к сложным задачам реального мира.

Вещественные числа типа float и double всегда казались магией, ведь кажется, что они могут хранить всё! Но это далеко не так и для реализации систем надежных вычислений нужно понимать, как они работают. Лучший способ это понять - это написать собственную библиотеку, которая сможет проходить тесты стандарта IEEE 754. В докладе будет рассмотрен опыт реализации умножения таких чисел и тесты для этого. Также рассмотрим статью на SPIN2019, в которой было предложено верифицировать такие вычисления методом Model Checking и оценим число состояний для такой реализации.

In this talk, I will present an overview of the Finite Countermodel Method (FCM), a powerful approach to the verification of infinite-state and parameterized systems. I will demonstrate multiple applications of the method and will discuss its relative completeness with respect to methods based on regular invariants.

Доклад представляет собой обзор языка Verilog — одного из ключевых языков описания аппаратуры (HDL). Рассматриваются основные концепции и конструкции языка, его роль в проектировании, моделировании и верификации цифровых систем, включая использование формальных методов.

Доклад содержит обзор системы K, позволяющей порождать полезные инструменты (парсер, интерпретатор, дедуктивный верификатор) на основе синтаксиса и семантики языка программирования. Будет рассказано об идеологии проекта, о том, как пользоваться основными элементами системы, а также о примерах её применения на практике.

Обычно курс по дедуктивной верификации рассказывает о верификации итеративных программ, спецификации которых могут содержать функции, заданные рекурсивно. Но в этом докладе будет рассказано для студентов как специфицировать программы с рекурсией, что такое табличные доказательства, и как они возникают при верификации рекурсивных программ.

Доклад содержит обзор работ конференции FormaliSE 2024 - ежегодной конференции, посвящённой работам на пересечении формальных методов и разработки.

Более подробно будет рассмотрена статья "A Semantics of Structures, Unions, and Underspecified Terms for Formal Specification" (Louis Gauthier, Virgile Prevosto, Julien Signoles, 2024). В этой работе предлагается формализация семантики для части языка ACSL. ACSL - язык спецификации для C, используемый в наборе инструментов верификации Frama-C для аннотации кода. На момент начала работы семантика ACSL не была формально описана, что позволяло неоднозначно трактовать спецификации. Эта статья представляет собой первый этап формализации семантики на Coq. Приведённая семантика основана на семантикe языка C, предложенной в "The C Standard Formalized in Coq" (R. Krebbers, 2015). Наибольшее внимание в статье уделено описанию семантики равенства структур, объединений и логике обработки не полностью специфицированных термов, эти темы не были рассмотрены ранее в других статьях, посвящённых языкам спецификации.

Наконец-то и в России появились пока небольшие группы специалистов, применяющих формальные методы в производственном программировании. Назрела необходимость объединения специалистов для решения существующих проблем в сфере формальных методов на государственном уровне. Предлагаемая форма объединения – ассоциация специалистов, считающих формальные методы своей профильной дисциплиной.

В докладе будет представлен анализ по следующим аспектам:

• позиция научной дисциплины «Формальные методы» в системе наук;
• краткое определение формальных методов: понятия задачи, спецификации, верификации и т.д.
• области применения формальных методов;
• состояние исследований и применений формальных методов в нашей стране;
• проблемы обучения формальным методам;
• основные задачи развития дисциплины исходя из текущего состояния.

В нашей работе мы исследуем изменения взаимодействующих через каналы FIFO-машин, формализующих поведение акторов коммуникационных протоколов. Мотивацией нашей работы служит тот факт, что описание поведения акторов на специализированных языках программирования протоколов, может изменяться в силу различных причин, таких как изменение содержания сообщений, изменение условий или последовательности получения и отправки сообщений, изменение адресатов и т.п. Во всех этих случаях необходимо убедиться, что коммуникационный протокол, участником которого является изменившийся актор, по-прежнему остаётся корректным. Формальная верификация коммуникационных протоколов является ресурсоёмкой процедурой, поэтому целесообразно определить безопасные изменения поведения акторов, сохраняющие корректность протокола. В этой работе мы рассматриваем класс мутаций акторов, который предполагает включение поведений акторов, т.е. мутировавший актор выполняет только часть работы оригинального актора.