Все семинары

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

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

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

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

Становление Новосибирской экономико-социологической школы тесно связано с именами академика Татьяны Ивановны Заславской и д.э.н. Розалины Владимировны Рывкиной. Визитной карточкой школы стали сельские/аграрные исследования, старт которым в середине 1960-х дал запрос новосибирских партийных органов о причинах массовой миграции сельского населения в города и способах сохранения трудового потенциала колхозов и совхозов. Чтобы ответить на поставленные вопросы, новосибирские социологи в кооперации с центральным статистическим управлением России (ЦСУ РСФСР) в 1967 г. опросили более 5000 сельских семей и собрали отсутствующую в ту пору информацию о социальной и производственной инфраструктуре сельских поселений Новосибирской области.

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

В 1990-е годы фокус и формат исследований кардинально поменялись. Социологам нужно было «держать руку на пульсе»: отслеживать первые ростки и проблемы развития фермерского движения; этапы слома колхозно-совхозной системы и массового появления «брошенных деревень», жители которых одномоментно остались без работы; процессы возврата к архаике натурального производства и обмена и неоотходничества. Постепенно внимание социологов переместилось на становление отношений частной собственности и последствия приватизации колхозов и совхозов, плюсов и минусов земельной реформы в контексте развития многоукладной аграрной экономики и эффективного (в кавычках или без) сельского хозяйства. Исследовались проблемы сельского развития, социальной дифференциации, плохо сбалансированного рынка труда.

Сегодня интерес социологов отдела прикован к новому витку «трансформации сельского пространства» в рамках проведения муниципальной реформы, которая нацелена на отмену в селах и деревнях местных администраций (или по-старому «сельсоветов») и превращения районов в муниципальные округа, а также создания по всей стране «сельских агломераций», переопределяющих перспективы сельского развития и судьбу сельских жителей. Другой важный сюжет для исследования – цифровизация государственного управления аграрным сектором и ее последствия. Исследуя эти темы, мы наблюдаем за тем, как государство пытается решать старые вопросы обустройства и управления сельским пространством на «новый лад», в том числе повторяя «ошибки прошлого» и совершая «новые помарки».

В этом докладе мы продолжим говорить про 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 получилось успешно применить для задачи верификации алгоритма поиска подстроки.

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

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

Обнаружен рост температуры поверхности Земли, который связывается с глобальным потеплением. Его главной причиной является антропогенная эмиссия парниковых газов, прежде всего, CO2. Основной вклад вносит энергетика на органическом топливе. Показано, что антропогенные выбросы ОРВ (озоноразрушающих веществ) типа фреонов приводят к разрушению озонового слоя Земли и образованию озоновых «дыр» в Антарктике. Разрушение озонового слоя и глобальное изменение климата взаимосвязаны, поскольку ОРВ и их заменители являются сильными парниковыми газами. Глобальное потепление сопровождается существенным ростом экстремальных климатических и погодных явлений.

Особую опасность представляют так называемые переломные моменты (tipping points), которые проявляются при превышении порогового значения параметров системы и могут привести к необратимым катастрофическим последствиям. Показано, что в текущей конфигурации Земля находится в бистабильном (мультистабильном) режиме - могут быть реализованы два асимптотических состояния. Теплое состояние (warm), в котором мы находимся, конкурирует с состоянием снежного кома (snowball). Бистабильность существует благодаря положительной обратной связи лед-альбедо. Необходимо дальнейшее развитие климатических моделей Земли с одновременной организацией систем климатического мониторинга.

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

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

19.11.2025 г. исполнится 125 лет со дня рождения одного из основателей и первого председателя Сибирского отделения АН СССР / СО РАН академика Михаила Алексеевича Лаврентьева (1900–1980). В докладе будут освещены ранние научные работы М.А. Лаврентьева, затронута «предыстория» физико-математических школ-интернатов.

Вещественные числа типа 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, позволяющей порождать полезные инструменты (парсер, интерпретатор, дедуктивный верификатор) на основе синтаксиса и семантики языка программирования. Будет рассказано об идеологии проекта, о том, как пользоваться основными элементами системы, а также о примерах её применения на практике.

В настоящее время известны 7 видов представителей семейства Ортокоронавирусов, вызывающих заболевания человека. Два из них были открыты в середине 60-х годов в европейских странах, один – в 2003 году в КНР, еще два – в 2004-2005 годах в Нидерландах и Гонконге, один – в Саудовской Аравии и Нидерландах в 2012 году. И пока последний SARS-CoV-2 – в КНР в 2020 году, который вызвал колоссальную пандемию, медленно завершившуюся в 2023 году, но при этом циркуляция данного вируса не прекратилась, а лишь кардинально снизилась его патогенность для человека.

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

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