 |
STEP-2024 |
|
|
Российский гибридный семинар STEP-2024
|
| Николай Вячеславович Шилов (Университет Иннополис): "Теория всего": унификация паттернов дизайна алгоритмов (метода отката, ветвей и границ, жадных алгоритмов, метода разделяй и властвуй, и динамического программирования...) | Аннотация: Курс проектирования и анализа алгоритмов является обязательной составляющей учебных программ по информатике всех уровней. В университетах этот курс обязательно включает изучение структур данных, методы проектирования алгоритмов, теорию сложности и т.д. Этот курс знакомит с такими методами проектирования алгоритмов, как жадные алгоритмы, динамическое программирование, метод разделяй и властвуй, метод отката, метод ветвей и границ. Обычно знакомство с этими методами происходит на примерах. Но они могут быть (полу)формализованы в виде рекурсивных "паттернов" (с использованием map и reduce), специфицированы условиями частичной и/или тотальной корректности и обоснованы (доказаны) методом Флойда верификации алгоритмов. | День, дата и время: среда 22 мая 2024 г. с 15:00 до 16:30 мск (19:00-20:30 в Новосибирске)
|
Семинар пройдет гибридно: в Университете Иннополис и онлайн (в Skype - можно смотреть в браузере). |
| Александр Иванович Легалов (Высшая школа экономики, Москва): Процедурно-параметрический полиморфизм и его интеграция с языком программирования C | Аннотация: Разработка больших программ часто связана с инкрементальным расширением уже написанного кода. При этом встречаются ситуации, когда альтернативные программные объекты формируются во время выполнения. В этом случае для их идентификации и последующей обработки используется либо явная проверка типа, либо один из методов динамического полиморфизма, предоставляемый тем или иным языком программирования. Расширение программы за счет новых альтернатив, добавляемых в ходе разработки, может привести к модификации уже написанного кода. В этих случаях для минимизации изменений вместо явной проверки типов обычно применяются методы динамического полиморфизма. Из них к широко известным можно отнести ОО полиморфизм, использование интерфейсов в Go и типажей в Rust. Процедурно-параметрический полиморфизм является альтернативным подходом. Рассматриваются его особенности и интеграция с языком программирования C. Представлены дополнительные синтаксические конструкции, ориентированные на поддержку подхода, их возможности и варианты реализации. Приводятся примеры эволюционного расширения кода для простых ситуаций демонстрирующие большую гибкость по сравнению с существующими подходами. Также рассматривается моделирование паттернов проектирования, повышение надежности за счет обертки над ненадежными языковыми конструкциями языка C. | День, дата и время: среда 29 мая 2024 г. с 15:00 до 16:30 мск (19:00-20:30 в Новосибирске)
|
Семинар пройдет онлайн (в Skype - можно смотреть в браузере). |
| По сложившейся традиции нашего семинара, мы информируем участников семинара о программе ежегодного Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE) и приглашаем присоединиться к заседаниям SYRCoSE очно или онлайн. | SYRCoSE
организуется ежегодно начиная с 2007 широко известными специалистами в программной инженерии и программировании Александром Константиновичем Петренко (Институт системного программирования РАН, Москва) и Андреем Николаевичем Тереховым (Санкт-Петербургский Государственный Университет).
Программа Коллоквиума SYRCoSE-2023 включает два пригашенных (пленарных) доклада:
|
Даты: среда 29 мая - пятница 1 июня 2024 г. | Для получения ссылки для подключения к трансляции SYRCoSE-2024 необходима регистрация. |
| Артем Сергеевич Бурмяков (Университет Иннополис): 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. | День, дата и время будут объявлены в середине июня 2024 г.
(Это будет заключительная третья часть доклада, первые две части были представлены на заседаниях семинара 6 марта и 24 апреля 2024. Есть рабочие записи на YouTube-канале ИСИ СО РАН первой и второй частей доклада, а также презентация доклада.) |
Семинар пройдет гибридно: в Университете Иннополис и онлайн (в Skype - можно смотреть в браузере). |
Прошедшие заседания семинара: (в порядке Last-In - First-Out):
| Евгений Александрович Зуев (Университет Иннополис): Modelling C++ inheritance and dynamic semantics using a C++ virtual machine | Аннотация: Доклад представляет экспериментальный программный стенд, предназначенный для моделирования ключевых свойств языка С++, включая механизмы наследования (единичного, множественного и виртуального) и полиморфизма. Стенд включает компилятор представительного подмножества языка С++ в низкоуровневый интерпретируемый язык IML и виртуальную машину, реализующую аспекты динамической семантики С++ в части полиморфизма (виртуальные функции с перекрытиями, динамическое приведение типов) и распределения динамической памяти. Стенд может использоваться как инструмент моделирования различных программных конфигураций для оценки эффективности применения моделируемых свойств С++. Проект выполняется группой студентов университета Иннополис под руководством автора доклада. | Дата: среда 8 мая 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.) |
| Ершовская лекция 2024 г. | 19 апреля - День Рождения Андрея Петровича Ершова. По сложившейся традиции мы приглашаем участников семинара присоединиться к
традиционной Ершовской лекции, организуемой Институтом систем информатики им. А.П. Ершова.
В 2024 г. лекцию прочитал член Правления ключевых ИТ-ассоциаций России – АПКИТ и Руссофт Владимир Васильевич Рубанов, тема лекции Риски и преимущества открытости исходных кодов вашего программного обеспечения. Аннотация: В докладе рассмотрен феномен открытого исходного кода (open-source) программных проектов. Будет представлен анализ основных движущих сил и типов участников открытых проектов. Приведены примеры важных проектов и участия различных компаний в их разработке. Центральное место доклада занимает анализ преимуществ и рисков, которые возникают в связи с открытием исходного кода того или иного продукта или компонента. Показано наличие оптимальной точки открытия кода (в плане момента времени и объема открытия) в зависимости от ситуации. Отклонение от такой точки для конкретного проекта приводит либо к "недооткрытию" (under-open-sourcing), либо к "переоткрытию" (over-open-sourcing), что непосредственно влияет на развитие продукта. Наконец, в докладе будет рассмотрена история участия в проектах с открытым кодом компании Huawei, которая из состояния отрицания необходимости открытия кода за считаные годы превратилась в одного из мировых лидеров open-source движения. |
Дата: четверг 18 апреля 2024 г. | Есть запись лекции на YouTube-канале ИСИ СО РАН. |
| Андрей Валентинович Климов (Институт прикладной математики им. М.В. Келдыша РАН, Москва): Научное наследие В.Ф. Турчина и его кибернетические основания математики | Аннотация: Научно-философское наследие Валентина Федоровича Турчина (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 января. | Ссылки на презентацию доклада В. Крйновича и на записи выступлений И.О. Пыльцына и Л. Меркина даны в колонке слева. |