Новости
Во вторник 16 декабря в 14.30 состоится заседание N 1022 Объединенного семинара "Конструирование и оптимизация программ" ИСИ СО РАН и НГУ (Руководитель: д.ф.-м.н, профессор В.Н. Касьянов).
Докладчик: С.В. Попов
Тема: Реферат статьи "InstructIE: A Bilingual Instruction-based Information Extraction Dataset
(Honghao Gui, Shuofei Qiao, Jintian Zhang, Hongbin Ye, Mengshu Sun, Lei Liang, Jeff Z. Pan, Huajun Chen, Ningyu Zhang)
(arxiv.org, 2024)"
Чтобы принять участие в семинаре, необходимо перейти по ссылке.
В четверг 11 декабря 2025 г. пройдет Объединенный семинар "Интеллектуальные системы" и "Системное программирование" ИСИ СО РАН и кафедры программирования НГУ (Руководители: д.ф.-м.н. Марчук А.Г., к.т.н. Загорулько Ю.А., к.ф.-м.н. Бульонков М.А.). Начало в 10:00. Место проведения: к. 254 ИСИ СО РАН.
Докладчик: Хайрулин Сергей Сергеевич (ИСИ СО РАН)
Тема: Алгоритмы и программный инструментарий обработки данных на гетерогенных вычислительных системах (представление кандидатской диссертации)
Ссылка на участие в семинаре онлайн
Внимание! Выставление зачета аспирантам и студентам – на основании ОЧНОГО посещения семинара.
Поздравляем Евгения Бодина, научного сотрудника лаборатории теоретического программирования (зав. лабораторией к.ф.м-н. А.В. Промский) с заслуженным призовым III местом в соревнованиях по стрельбе из пневматической винтовки VIII Спартакиады трудовых коллективов предприятий, учреждений Советского района и научных институтов СО РАН имени Е.А. Горланова, желаем дальнейших успехов!
Коллег приглашаем присоединиться к спортивной команде Института и участвовать в спортивных мероприятиях.
Профсоюз и Советы научной молодежи играют важную роль в поддержке и
развитии научного сообщества, обеспечивая эффективное взаимодействие между
его членами и способствуя улучшению условий труда и научной деятельности.
Совет научной молодежи (СНМ) служит важной платформой для объединения
научной молодежи: аспирантов и научных сотрудников в возрасте как правило
до 39 лет. Его основные цели: представление интересов молодых специалистов
в профессиональной сфере и решение актуальных социальных проблем. СНМ
способствует созданию и развитию коммуникаций между молодыми учеными из
различных научных центров, что позволяет обмениваться опытом, идеями и
находить совместные решения для достижения научных и социальных целей.
Молодежная комиссия Профсоюза СО РАН проводит анкетирование среди научной
молодежи для ее привлечения, поддержки и продвижения в состав СНМ и/или
Профсоюза. Результат анкетирования может быть использован первичными
профсоюзными организациями и СНМ для оптимизации их работы в вопросах
защиты трудовых прав, улучшения условий труда, создания благоприятного
психологического климата в коллективе организации.
Во вторник 9 декабря 2025 г. пройдет семинар "Теоретическое и экспериментальное программирование" (Руководитель: к.ф.-м.н., с.н.с. Гаранина Н.О., соруководители: к.ф.-м.н., н.с. Кондратьев Д.А., к.ф.-м.н., с.н.с. Ануреев И.С., секретарь: к.ф.-м.н. Шилов Н.В.).
Время проведения: 17.00-18.30 НСК (13.00-14.30 МСК) очно в к. 239 ИСИ СО РАН и онлайн по ссылке.
Анонсы, слайды докладов и другая информация будут доступны в группе телеграм.
Докладчик: Максим Вячеславович Нейзов (Институт Автоматики и Электрометрии СО РАН)
Тема: Loom: Использование симметрии при разработке и верификации программных реагирующих систем
Большое пространство состояний реальных программ затрудняет или делает невозможной их непосредственную верификацию методом проверки модели (model checking). Наличие симметрии в программе достаточно часто позволяет упростить модель и сократить её пространство состояний, что приводит к резкому снижению времени верификации. Классический подход состоит в обнаружении группы симметрии и построении на её основе упрощенной модели для верификации. Однако не все инструменты имеют поддержку симметрии, а инструменты с такой поддержкой не всегда справляются с поставленной задачей.
В докладе предлагается альтернативный классическому подход к разработке программ основанный на симметрии. В программе выделяется ядро – координационный центр, который работает с учётом симметрии и отвечает за выполнимость заданных темпоральных свойств.
Ядро координирует вычисления, которые вынесены за его пределы – в обвязку ядра. В связи с этим ядро имеет небольшое пространство состояний и может быть верифицировано методом проверки модели. Обвязка не может вмешиваться в работу верифицированного ядра и нарушать его свойства.
Подход продемонстрирован на примере разработки и верификации арбитра ресурсов марсохода. Арбитр координирует доступ n процессов к m ресурсам, где n и m -- натуральные числа. Используются язык программирования C/C++ и инструмент проверки модели Spin. Модель поведения ядра автоматически извлекается верификатором Spin из C-кода. Проверке подлежат темпоральные свойства, выраженные в логике LTL.
Три призовых места заняла наша команда в соревнованиях Профсоюза СО РАН по спортивному метанию ножей, которые состоялись 3 декабря: в командном первенстве 2-е призовое место, в личном зачёте среди мужчин Евгений Бодин занял 2-е призовое место, и Антонцева Марина завоевала призовое 2-е место в личном зачёте среди женщин.
Поздравляем и желаем дальнейших побед, а коллег Института приглашаем присоединиться к спортивной команде и участвовать в соревнованиях.
Новости за последний месяц
