 |
STEP-2024 |
|
|
Российский гибридный семинар STEP-2024
|
| Ершовская лекция 2024 г. |
19 апреля - День Рождения Андрея Петровича Ершова. По сложившейся традиции мы приглашаем участников семинара присоединиться к
традиционной Ершовской лекции, организуемой Институтом систем информатики им. А.П. Ершова.
В 2024 г. лекцию прочитает член Правления ключевых ИТ-ассоциаций России – АПКИТ и Руссофт Владимир Васильевич Рубанов, тема лекции Риски и преимущества открытости исходных кодов вашего программного обеспечения. Аннотация: В докладе будет рассмотрен феномен открытого исходного кода (open-source) программных проектов. Будет представлен анализ основных движущих сил и типов участников открытых проектов. Приведены примеры важных проектов и участия различных компаний в их разработке. Центральное место доклада занимает анализ преимуществ и рисков, которые возникают в связи с открытием исходного кода того или иного продукта или компонента. Показано наличие оптимальной точки открытия кода (в плане момента времени и объема открытия) в зависимости от ситуации. Отклонение от такой точки для конкретного проекта приводит либо к "недооткрытию" (under-open-sourcing), либо к "переоткрытию" (over-open-sourcing), что непосредственно влияет на развитие продукта. Наконец, в докладе будет рассмотрена история участия в проектах с открытым кодом компании Huawei, которая из состояния отрицания необходимости открытия кода за считаные годы превратилась в одного из мировых лидеров open-source движения. |
День, дата и время: четверг 18 апреля 2024 г. 15:00-17:30 в Новосибирске (11:00-12:30 мск). | Лекция пройдет гибридно: в 3107 аудитории Новосибирского государственного университета и онлайн (ссылка для подключения будет объявлена позже). |
| Артем Сергеевич Бурмяков (Университет Иннополис): Towards a Tractable Exact Test for Global Multiprocessor Fixed Priority Scheduling (вторая часть) | Аннотация: An exact schedulability analysis of a system of sporadic tasks to be executed upon a multiprocessor platform is proved to be a weakly NP-hard computational problem. The available exact tests suffer from a high computation time and memory requirement, which make them intractable for large realistic real-time systems. On the other hand, the available approximate sufficient tests, which are faster and consume less memory, are very pessimistic in provisioning the execution requirements of a given system. Motivated by these observations, we propose an exact schedulability test for constrained-deadline sporadic tasks under global multiprocessor fixed-priority scheduler (GFP), which is significantly faster and consumes less memory, compared to any other available exact test. To derive a faster test, we exploit the idea of a state-space pruning, aiming at reducing the number of feasible system states to be examined by the test. The resulted test is multiple orders of magnitude faster with respect to other state-of-the-art exact tests. The C++ implementation of our test is publicly available. | День, дата и время: среда 24 апреля 2024 г. 16:00-17:30 мск (20:00-21:30 в Новосибирске).
(Это будет продолжение доклада, представленного на заседании семинара 6 марта 2024. Есть рабочая запись на YouTube-канале ИСИ СО РАН и презентация первой части доклада.) |
Семинар пройдет гибридно: в 422 аудитории Университета Иннополис и онлайн (в Skype - можно смотреть в браузере). |
Прошедшие заседания семинара: (в порядке Last-In - First-Out):
| Андрей Валентинович Климов (Институт прикладной математики им. М.В. Келдыша РАН, Москва): Научное наследие В.Ф. Турчина и его кибернетические основания математики | Аннотация: Научно-философское наследие Валентина Федоровича Турчина (14.02.1931–07.04.2010) состоит из трех частей:
(1) философской, объясняющей его эволюционную концепцию с центральным понятием метасистемного перехода как кванта эволюции, — книга "Феномен науки: Кибернетический подход к эволюции" [1977 (англ.), 1993, 2003 (рус.)]; (2) социальной: обсуждение эволюции общества и человека — книга "Инерция страха: Социализм и тоталитаризм" [1977]; (3) научной: суперкомпиляция в программировании и кибернетические основания математики — статья "A constructive interpretation of the full set theory" [1987] и отчеты "The Cybernetic Foundation of Mathematics" [1983]. В докладе кратко охарактеризованы первые части, суперкомпиляция опущена и дано введение в кибернетические основания математики — потенциалистской интерпретации, являющейся расширением алгоритмического конструктивизма А.А. Маркова и Э. Бишопа путем введения (модели) математика в теорию — таким образом, что удалась конструктивная интерпретация теории множеств ZF. |
Дата: среда 10 апреля 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Александр Валентинович Когтенков: Объектно-ориентированное программирование без встроенных типов | Аннотация: Насколько оправдано упрощение объектно-ориентированного языка программирования при доказательстве каких-то его свойств? Что можно написать на ОО языке без встроенных типов, арифметических операторов, операторов сравнения, условных инструкций и инструкций цикла? Теоретически возможность объявлять классы, переменные и процедуры, а также создавать и присваивать объекты, обращаться к переменным и вызывать процедуры должно хватить, чтобы реализовать любую программу. Но как это выглядит на практике? На семинаре будет разобран код простого примера, отвечающего на этот вопрос.
Несмотря на фундаментальную природу, работа не носит научного характера, доступна широкому кругу специалистов профильных специальностей, может быть интересна разработчикам и исследователям языков программирования и трансляторов. |
Дата: среда 3 апреля 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Алексей Юрьевич Зубарев (Институт систем информатики СО РАН, Новосибирск): Взаимосвязи семантик и эквивалентностей непрерывно-временных сетей Петри со слабой временной стратегией | Аннотация: Непрерывно-временные сети Петри — это расширение сетей Петри, в которых каждому переходу ставятся в соответствие временной интервал его срабатывания и локальные часы. Данная модель позволяет учитывать как функциональные (качественные), так и реально-временные (количественные) свойства моделируемых систем. Рассматриваются непрерывно-временные сети Петри со слабой временной стратегией, где ход модельного времени не форсирует срабатывания сетевых переходов. Для данной модели и ее модификаций разрабатываются и исследуются семантические представления и поведенческие эквивалентности в дихотомиях «интерливинг-частичный порядок» и «линейное-ветвящееся время». Кроме того, в контексте «слабых» непрерывно-временных сетей Петри предлагается метод редукции пространства состояний за счёт их дискретизации. | Дата: среда 20 марта 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Маргарита Владимировна Коровина (Институт систем информатики СО РАН, Новосибирск): Automated Reasoning with Continuous Data | Семинар STEP-2024 продолжает традицию специальных заседаний в Международный женский день: ru-STEP-2021, ru-STEP-2022 и STEP-2023.
Аннотация доклада In this talk we report on ongoing research on solving non-linear constraints over the reals occurring in a wide range of applications, starting with program verification, ranging over verification of real-world designs all the way to automation of formally verified proofs of mathematical statements. In our framework methods from Computable Analysis and Automated Reasoning are combined to meet efficiency and expressiveness. This approach is applicable to a large number of constraints involving computable non-linear functions, piecewise polynomial splines, transcendental functions and solutions of polynomial differential equations. We give an introduction to the ksmt calculus for checking satisfiability of non-linear constraints in a CDCL style way inspired by advances in SAT solving. Along proof search ksmt resolves two types of conflicts: linear and non-linear. Linear conflicts are delegated to a decision procedure for linear real arithmetic and non-linear conflicts are resolved by local linearisations separating the solution set and the current conflict. We show that the ksmt calculus is a σ-complete decision procedure for bounded problems. |
Дата: среда 28 февраля 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. |
| Всеслав Станиславович Секорин (Тверской государственный университет): Выразительные возможности операторов частичной неподвижной точки для конечных и бесконечных систем | Аннотация: В работе рассмотрены различные семантики частичной фиксированной точки для конечных и бесконечных алгебраических систем. В частности, показано, что операторы частичной фиксированной точки рассматриваемых семантик можно промоделировать оператором инфляционной фиксированной точки в тех алгебраических системах, в которых есть строгий частичный порядок со сколь угодно длинными цепями. Также, например, показано что элиминировать оператор частичной фиксированной точки можно только в тех теориях, в которых любой такой оператор зацикливается за конечное число шагов. Доклад представляет материалы и результаты кандидатской диссертации на соискание ученой степени кандидата физико-математических наук по специальности 1.1.5. "Математическая логика, алгебра, теория чисел и дискретная математика". | Дата: среда 28 февраля 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Игорь Сергеевич Ануреев (Институт систем информатики СО РАН, Новосибирск): Логика распознавания последовательностей состояний SSRL (State Sequences Recognition Logic) и примеры её применения для формализации темпоральных требований к управляющим программ | Аннотация: Предлагается формализм для описания свойств последовательностей состояний, порождаемых системой переходов (state transition system). Этот формализм под рабочим названием SSRL (State Sequences Recognition Logic) позволяет задавать свойства поведения системы переходов, определяемого как множество последовательностей состояний, порождаемых отношением перехода. В отличие от LTL, он поддерживает императивные вставки, позволяющие сохранять информацию в именованных компонентах состояний (аналог let в функциональных языках программирования), называемых атрибутами. В тоже время он имеет более простую систему модальностей и более жесткий порядок их комбинирования по сравнению с LTL. Даются методология и примеры его применения для формализации темпоральных требований к управляющим программ, на которые он, в первую очередь, ориентирован. Цель разработки формализма применительно к решению этой задачи - расширить область применимости ранее представленного на семинаре формализма EDTL (Event-Driven Temporal Logic), который позиционируется как язык описания темпоральных требований, ориентированный на инженеров. В качестве обоснования большей выразительной силы нового формализма рассматриваются примеры требований, невыразимых на EDTL, а также определяется формальная семантика EDTL на SSRL. | Дата: среда 14 февраля 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Алексей Недоря: О "граблях" в инициализации объектов в современных языках программирования | Аннотация: Рассмотрены инициализации объектов в современных языках программирования Swift/Kotlin/Тривиль. (Выступление в рамках темы "филология программирования", поднятой А.В. Коноваловым во время "Дня Проблем 2023", про язык Тривиль см. выступления Алексей Недори "Опыт разработки и реализации языка Тривиль" и "Интенсивное программирование: язык Тривиль" на семинаре STEP-2023.) | Дата: пятница 2 февраля 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Заседание семинара посвященное Всемирному Дню Логики (https://en.wikipedia.org/wiki/World_Logic_Day) |
В 2024 г. мы продолжили традицию семинара (см. Logic Day 2023, Logic Day 2022 и
Logic Day 2021)
совместных заседаний с
Математическим Клубом Университета Иннополис (см. Telegram-беседу Logic Day in Innopolis ).
А так как Всемирный День Логики установлен UNESCO (United Nations Educational, Scientific and Cultural Organization), то у нас были сообщения по спектру тем Education, Science, Culture…
|
Обычно мы выбираем дату так, что бы не конкурировать с другими событиями в честь Всемирного Дня Логики. Наш встреча состоялась вечером в пятницу 26 января и утром в субботу 27 января. | Ссылки на презентацию доклада В. Крйновича и на записи выступлений И.О. Пыльцына и Л. Меркина даны в колонке слева. |