Все семинары

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

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

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

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

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

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

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

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

Ответ попытается дать к.и.н. А.И. Савин, соавтор новой политической биографии Леонида Брежнева, опубликованной в конце 2024 г.

В этом докладе мы рассмотрим исторические корни, последние достижения и будущие перспективы современных оптических стандартов частоты. Кратко будут обсуждаться некоторые новые методы и подходы в прецизионной лазерной спектроскопии запрещенных переходов в ультрахолодных атомах и ионах с акцентом на вклад Института лазерной физики СО РАН.

В 1996 году физик-теоретик Дэвид Ди Винченцо из IBM сформулировал минимальные требования, необходимые для того, чтобы построить квантовый компьютер. На пути реализации технически состоятельных конструкций квантового компьютера, основанного на любом из требований, стоит огромное количество трудностей, которые ученые и инженеры постепенно преодолевают. В докладе речь пойдет о физических принципах работы квантовых компьютеров на примере экспериментальной установки в ИФП СО РАН.

В начале 20 века большинство физиков не верило в существование атомов, потому что всё, что меньше длины волны света, невозможно увидеть. Физическая теория считалась полностью завершённой. Как получилось, что возникла необходимость в концептуально новой теории? Почему события из детерминированных стали вероятностными? Что легло в основу квантовой теории? Об этом в докладе «Квантовая механика : от наблюдений к теории».

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

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

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

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