Семинары

Все семинары

В четверг 27 ноября 2025 г. пройдет Объединенный семинар "Интеллектуальные системы" и "Системное программирование" ИСИ СО РАН и кафедры программирования НГУ (Руководители: д.ф.-м.н. Марчук А.Г., к.т.н. Загорулько Ю.А., к.ф.-м.н. Бульонков М.А.). Начало в 10:00. Место проведения: к. 254 ИСИ СО РАН.

Докладчик: Марчук Александр Гурьевич, д.ф-м.н., профессор, ИСИ СО РАН
Тема: Язык программирования Rust: новая модель работы с памятью

Ссылка на участие в семинаре онлайн

Внимание! Выставление зачета аспирантам и студентам – на основании ОЧНОГО посещения семинара.

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

Во вторник 25 ноября 2025 г. пройдет семинар "Теоретическое и экспериментальное программирование" (Руководитель: к.ф.-м.н., с.н.с. Гаранина Н.О., соруководители: к.ф.-м.н., н.с. Кондратьев Д.А., к.ф.-м.н., с.н.с. Ануреев И.С., секретарь: к.ф.-м.н. Шилов Н.В.).

Время проведения: 17.00-18.30 НСК (13.00-14.30 МСК) очно в к. 239 ИСИ СО РАН и онлайн по ссылке.

Анонсы, слайды докладов и другая информация будут доступны в группе телеграм.

Докладчик: Виталий Курин (Neapolis University Pafos)
Тема: Платформа для разработки Фундаментальных Мульти-Модальных Систем Верификации

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

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

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

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

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

В четверг 20 ноября 2025 г. пройдет Объединенный семинар "Интеллектуальные системы" и "Системное программирование" ИСИ СО РАН и кафедры программирования НГУ (Руководители: д.ф.-м.н. Марчук А.Г., к.т.н. Загорулько Ю.А., к.ф.-м.н. Бульонков М.А.). Начало в 10:00. Место проведения: к. 254 ИСИ СО РАН.

Докладчик: Сидорова Елена Анатольевна, Ильина Дарья Владимировна (ИСИ СО РАН, НГУ)
Тема: XXII Национальная конференция по искусственному интеллекту с международным участием (КИИ-2025). Часть 3

Ссылка на участие в семинаре онлайн

Внимание! Выставление зачета аспирантам и студентам – на основании ОЧНОГО посещения семинара.

Сергей Владимирович Алексеенко

25 ноября в 11:00 в каб. 3-115 (конференцзал ИВМиМГ СО РАН) состоится очередное заседание Методологического семинара ИСИ СО РАН совместно с ИВМиМГ СО РАН.

Докладчик: Сергей Владимирович Алексеенко, доктор физико-математических наук, академик РАН, научный руководитель Института теплофизики им. С.С. Кутателадзе СО РАН
Тема доклада: «Изменения климата: экстремальные и катастрофические климатические явления, взаимосвязи с энергетикой»

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

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

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

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

Ссылка на дистанционное подключение:
https://1jy0brqx.ktalk.ru/j9nk0nc9mxv4
PIN-код: 6727

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

Во вторник 18 ноября 2025 г. пройдет семинар "Теоретическое и экспериментальное программирование" (Руководитель: к.ф.-м.н., с.н.с. Гаранина Н.О., соруководители: к.ф.-м.н., н.с. Кондратьев Д.А., к.ф.-м.н., с.н.с. Ануреев И.С., секретарь: к.ф.-м.н. Шилов Н.В.).

Время проведения: 17.00-18.30 НСК (13.00-14.30 МСК) очно в к. 239 ИСИ СО РАН и онлайн по ссылке.

Анонсы, слайды докладов и другая информация будут доступны в группе телеграм.

Докладчики: Бельтюков Анатолий Петрович (профессор, Удмуртский государственный университет, Институт математики, информационных технологий и физики) и Милад Джудакизаде (аспирант, Удмуртский государственный университет)
Тема: Дедуктивный синтез программ в логическом программировании

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

Объединенный семинар "Конструирование и оптимизация программ"

Во вторник 18 ноября в 14.30 состоится заседание N 1020 Объединенного семинара "Конструирование и оптимизация программ" ИСИ СО РАН и НГУ (Руководитель: д.ф.-м.н, профессор В.Н. Касьянов).

Докладчик: Г.Ю. Дедов
Тема: Реферат статьи "Demystifying NCCL: An In-depth Analysis of GPU Communication Protocols and Algorithms (Zhiyi Hu, Siyuan Shen, Tommaso Bonato, Sylvain Jeaugey, Cedell Alexander, Eric Spada, Jeff Hammond, Torsten Hoefle) (arxiv.org, 2025)"

Чтобы принять участие в семинаре, необходимо перейти по ссылке.

В четверг 13 ноября 2025 г. пройдет Объединенный семинар "Интеллектуальные системы" и "Системное программирование" ИСИ СО РАН и кафедры программирования НГУ (Руководители: д.ф.-м.н. Марчук А.Г., к.т.н. Загорулько Ю.А., к.ф.-м.н. Бульонков М.А.). Начало в 10:00. Место проведения: к. 254 ИСИ СО РАН.

Докладчик: Загорулько Юрий Алексеевич (ИСИ СО РАН, НГУ)
Тема: XXII Национальная конференция по искусственному интеллекту с международным участием (КИИ-2025). Часть 2

Ссылка на участие в семинаре онлайн

Внимание! Выставление зачета аспирантам и студентам – на основании ОЧНОГО посещения семинара.

Николай Вячеславович Шилов

18 ноября в 11:00 в каб. 239 состоится очередное заседание Методологического семинара ИСИ СО РАН.

Докладчик: Николай Вячеславович Шилов, к.ф.-м.н., независимый исследователь
Тема доклада: «Молодой математик Михаил Алексеевич Лаврентьев»

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

Ссылка на дистанционное подключение:
https://telemost.yandex.ru/j/99119182798336

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

Во вторник 11 ноября 2025 г. пройдет семинар "Теоретическое и экспериментальное программирование" (Руководитель: к.ф.-м.н., с.н.с. Гаранина Н.О., соруководители: к.ф.-м.н., н.с. Кондратьев Д.А., к.ф.-м.н., с.н.с. Ануреев И.С., секретарь: к.ф.-м.н. Шилов Н.В.).

Время проведения: 17.00-18.30 НСК (13.00-14.30 МСК) очно в к. 239 ИСИ СО РАН и онлайн по ссылке.

Анонсы, слайды докладов и другая информация будут доступны в группе телеграм.

Докладчик: Сергей Михайлович Старолетов (с.н.с. Института Автоматики и Электрометрии СО РАН, доцент АлтГТУ)
Тема: Вещественная арифметика IEEE 754, подходы к тестированию и верификации

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

В четверг 6 ноября 2025 г. пройдет Объединенный семинар "Интеллектуальные системы" и "Системное программирование" ИСИ СО РАН и кафедры программирования НГУ (Руководители: д.ф.-м.н. Марчук А.Г., к.т.н. Загорулько Ю.А., к.ф.-м.н. Бульонков М.А.). Начало в 10:00. Место проведения: к. 254 ИСИ СО РАН.

Докладчик: Загорулько Юрий Алексеевич (ИСИ СО РАН, НГУ)
Тема: XXII Национальная конференция по искусственному интеллекту с международным участием (КИИ-2025). Часть 1

Ссылка на участие в семинаре онлайн

Внимание! Выставление зачета аспирантам и студентам – на основании ОЧНОГО посещения семинара.

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

В пятницу 7 ноября 2025 г. пройдет семинар "Теоретическое и экспериментальное программирование" (Руководитель: к.ф.-м.н., с.н.с. Гаранина Н.О., соруководители: к.ф.-м.н., н.с. Кондратьев Д.А., к.ф.-м.н., с.н.с. Ануреев И.С., секретарь: к.ф.-м.н. Шилов Н.В.).

Семинар будет совмещён с приглашённой лекцией на контесте по формальной верификации VeHa-2025, поэтому пройдет полностью онлайн и состоится в необычный день и время: в пятницу 7 ноября в 16:00 мск (20:00 нск).

Докладчик: Alexei Lisitsa (School of Computer Science and Informatics, University of Liverpool)
Тема: Finite Countermodel Finding for Infinite State and Parametrized Verification

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.

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

Ссылка на подключение — постоянная: https://telemost.yandex.ru/j/28529522210499

В четверг 30 октября 2025 г. пройдет Объединенный семинар "Интеллектуальные системы" и "Системное программирование" ИСИ СО РАН и кафедры программирования НГУ (Руководители: д.ф.-м.н. Марчук А.Г., к.т.н. Загорулько Ю.А., к.ф.-м.н. Бульонков М.А.). Начало в 10:00. Место проведения: к. 254 ИСИ СО РАН.

Докладчик: Марчук Александр Гурьевич (ИСИ СО РАН, НГУ)
Тема: Модель описания и решения задач, основанная на ТРИЗ

Ссылка на участие в семинаре онлайн

Внимание! Выставление зачета аспирантам и студентам – на основании ОЧНОГО посещения семинара.

Объединенный семинар "Конструирование и оптимизация программ"

Во вторник 4 ноября в 14.30 состоится заседание N 1019 Объединенного семинара "Конструирование и оптимизация программ" ИСИ СО РАН и НГУ (Руководитель: д.ф.-м.н, профессор В.Н. Касьянов).

Докладчик: Т.А. Золотухин
Тема: Visual Graph: текущие результаты и дальнейшее развитие проекта

Чтобы принять участие в семинаре, необходимо перейти по ссылке.

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

Во вторник 28 октября 2025 г. пройдет семинар "Теоретическое и экспериментальное программирование" (Руководитель: к.ф.-м.н., с.н.с. Гаранина Н.О., соруководители: к.ф.-м.н., н.с. Кондратьев Д.А., к.ф.-м.н., с.н.с. Ануреев И.С., секретарь: к.ф.-м.н. Шилов Н.В.).

Время проведения: 17.00-18.30 НСК (13.00-14.30 МСК) очно в к. 239 ИСИ СО РАН и онлайн по ссылке.

Анонсы, слайды докладов и другая информация будут доступны в группе телеграм.

Докладчик: Разбитнова Юлия Юрьевна, студент 2-го курса магистратуры ММФ НГУ
Тема: Язык Verilog: от описания аппаратуры до формальной верификации

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

Вниманию участников семинара! Так как следующий вторник 4 ноября — День народного единства, то семинар пройдет или в четверг 6 ноября, или в пятницу 7 ноября, день, время , тема и докладчик будут объявлены заранее.

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

Во вторник 21 октября 2025 г. пройдет семинар "Теоретическое и экспериментальное программирование" (Руководитель: к.ф.-м.н., с.н.с. Гаранина Н.О., соруководители: к.ф.-м.н., н.с. Кондратьев Д.А., к.ф.-м.н., с.н.с. Ануреев И.С., секретарь: к.ф.-м.н. Шилов Н.В.).

Время проведения: 17.00-18.30 НСК (13.00-14.30 МСК) очно в к. 239 ИСИ СО РАН и онлайн по ссылке.

Анонсы, слайды докладов и другая информация будут доступны в группе телеграм.

Докладчик: Бояндин Лев Константинович, студент 3-го курса бакалавриата ММФ НГУ
Тема: Краткий экскурс в K Framework

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

Сергей Викторович Нетесов

21 октября в 10:30 в каб. 239 состоится очередное заседание Методологического семинара ИСИ СО РАН.

Докладчик: Сергей Викторович Нетесов, зав. лабораторией, д.б.н., профессор, академик РАН, Новосибирский государственный университет
Тема доклада: «Гипотезы о происхождении вируса SARS-CoV-2 и его вариантов»

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

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

Ссылка на дистанционное подключение:
https://telemost.yandex.ru/j/88143475564360

В четверг 16 октября 2025 г. пройдет Объединенный семинар "Интеллектуальные системы" и "Системное программирование" ИСИ СО РАН и кафедры программирования НГУ (Руководители: д.ф.-м.н. Марчук А.Г., к.т.н. Загорулько Ю.А., к.ф.-м.н. Бульонков М.А.). Начало в 10:00. Место проведения: к. 254 ИСИ СО РАН.

Докладчик: Хамза Салем (Университет Иннополис)
Тема: Алгоритмический фреймворк для точного извлечения основного содержимого с новостных веб-сайтов (An Algorithmic Framework for Precise Main Content Extraction from News Websites)

Ссылка на участие в семинаре онлайн

Внимание! Выставление зачета аспирантам и студентам – на основании ОЧНОГО посещения семинара.

Объединенный семинар "Конструирование и оптимизация программ"

Во вторник 21 октября в 14.30 состоится заседание N 1018 Объединенного семинара "Конструирование и оптимизация программ" ИСИ СО РАН и НГУ (Руководитель: д.ф.-м.н, профессор В.Н. Касьянов).

Докладчик: Д.В. Андреев
Тема: Реферат статьи "Disco: A Compact Index for LSM-trees (Wenshao Zhong, Chen Chen, Xingbo Wu, Jakob Eriksson)(Proceedings of the ACM on Management of Data, Volume 3, Issue 1, Article No.: 33, Pages 1-27, 2025)"

Чтобы принять участие в семинаре, необходимо перейти по ссылке.

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

Во вторник 14 октября 2025 г. пройдет семинар "Теоретическое и экспериментальное программирование" (Руководитель: к.ф.-м.н., с.н.с. Гаранина Н.О., соруководители: к.ф.-м.н., н.с. Кондратьев Д.А., к.ф.-м.н., с.н.с. Ануреев И.С., секретарь: к.ф.-м.н. Шилов Н.В.).

Время проведения: 17.00-18.30 НСК (13.00-14.30 МСК) очно в к. 239 ИСИ СО РАН и онлайн по ссылке.

Анонсы, слайды докладов и другая информация будут доступны в группе телеграм.

Докладчик: Николай Вячеславович Шилов (преподаватель Лицея 22 "Надежда Сибири")
Тема: Студент! Учись доказывать рекурсивные программы правильно!

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

Крайнева Ирина Александровна

7 октября в 11:00 в каб. 239 состоится очередное заседание Методологического семинара ИСИ СО РАН.

Докладчик: Ирина Александровна Крайнева, д.и.н., в.н.с. лаборатории информационных систем ИСИ им. А.П. Ершова СО РАН
Тема доклада: «Юрий Борисович Румер: биография как пазл»

Доклад посвящен физику-теоретику Ю.Б. Румеру (1901–1985), его сложной и одновременно необычной судьбе. Ровесник века, он участвовал в экспорте революции, становлении квантовой физики, подвергся репрессиям в годы Большого террора, создавал академическую науку в Сибири, учил студентов теории унитарной симметрии, писал учебники. На всю жизнь он сохранил память о Гёттингене, где провел три года в обществе М. Борна, встречался с А. Эйнштейном, которому его прочили в помощники. В Германии Румер познакомился в Л.Д. Ландау, с ним разделил дружбу, работу и заточение. После освобождения и реабилитации Юрий Борисович поселился в новосибирском Академгородке, где его еще помнят. Его питомцы-теоретики работают по всему миру, они по сей день вспоминают с трепетом, что были в двух рукопожатиях от Эйнштейна, отмечают эрудицию, скромность, порядочность, европейский стиль Юрия Борисовича, которые он сохранил несмотря на годы, проведенные в шарашке и ссылке.

Ссылка на дистанционное подключение:
https://telemost.yandex.ru/j/28195834907584

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

Во вторник 7 октября 2025 г. пройдет семинар "Теоретическое и экспериментальное программирование" (Руководитель: к.ф.-м.н., с.н.с. Гаранина Н.О., соруководители: к.ф.-м.н., н.с. Кондратьев Д.А., к.ф.-м.н., с.н.с. Ануреев И.С., секретарь: к.ф.-м.н. Шилов Н.В.).

Время проведения: 17.00-18.30 НСК (13.00-14.30 МСК) очно в к. 239 ИСИ СО РАН и онлайн по ссылке.

Анонсы, слайды докладов и другая информация будут доступны в группе телеграм.

Докладчик: магистрант СПбГУ Мищенко Станислав
Тема: Обзор конференции FormaliSE 2024 и реферат статьи "A Semantics of Structures, Unions, and Underspecified Terms for Formal Specification"

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

Объединенный семинар "Конструирование и оптимизация программ"

Во вторник 7 октября в 14.30 состоится заседание N 1017 Объединенного семинара "Конструирование и оптимизация программ" ИСИ СО РАН и НГУ (Руководитель: д.ф.-м.н, профессор В.Н. Касьянов).

Докладчик: В.Н. Касьянов
Тема: XXVII Всероссийская конференция "Научный сервис в сети Интернет" (22-25 сентября 2025 г.)

Чтобы принять участие в семинаре, необходимо перейти по ссылке.

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

Во вторник 30 сентября 2025 г. пройдет семинар "Теоретическое и экспериментальное программирование" (Руководитель: к.ф.-м.н., с.н.с. Гаранина Н.О., соруководители: к.ф.-м.н., н.с. Кондратьев Д.А., к.ф.-м.н., с.н.с. Ануреев И.С., секретарь: к.ф.-м.н. Шилов Н.В.).

Время проведения: 17.00-18.30 НСК (13.00-14.30 МСК) очно в к. 239 ИСИ СО РАН и онлайн по ссылке.

Анонсы, слайды докладов и другая информация будут доступны в группе телеграм.

Докладчик: к.т.н., с.н.с. Шелехов Владимир Иванович (ИСИ СО РАН)
Тема: Предпосылки создания ассоциации формальных методов

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

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

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

В четверг 25 сентября 2025 г. пройдет Объединенный семинар "Интеллектуальные системы" и "Системное программирование" ИСИ СО РАН и кафедры программирования НГУ (Руководители: д.ф.-м.н. Марчук А.Г., к.т.н. Загорулько Ю.А., к.ф.-м.н. Бульонков М.А.). Начало в 10:00. Место проведения: к. 254 ИСИ СО РАН.

Докладчик: Сидорова Е.А., Ильина Д.В. (ИСИ СО РАН)
Тема: Классификация аргументов с помощью больших языковых моделей

Ссылка на участие в семинаре онлайн

Внимание! Выставление зачета аспирантам и студентам – на основании ОЧНОГО посещения семинара.