 |
ru-STEP по-русски |
|
|
Архив Российского гибридного семинара ru-STEP (21.10.2020-08.02.2023)
|
| Итоговое заседание семинара | Семинар ruSTEP работал более двух с половиной лет, поэтому возникла необходимость обсудить некоторые накопившиеся проблемы.
Поэтому повестка включала следующие вопросы (которые представил Н.В. Шилов):
|
Дата: среда 8 февраля 2023 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН (включая выступление Юлии Владимировны). (Есть презентации к выступлению Н.В. Шилова и доклада Юлии Сергеевны Владимировой.) |
| Николай Вячеславович Шилов (Университет Иннополис): Введение в субструктурные логики (в продолжение Дня Логики 2023) | Аннотация: Во время выступление Обзор событий Всемирного Дня Логики 2023, которые мне удалось посетить онлайн на заседании семинара по случаю "Дня Логики 2023" я коротко рассказал о докладе Paradox and Substructurality Элиа Дзардини на семинаре Формальная философия 13 января 2023 г. Так как у участников нашего семинара ruSTEP возникло желание лучше познакомиться со субструктурными логиками, я решил подготовить это вводное ознакомительное выступление. | Дата: среда 1 февраля 2023 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.) |
| Заседание семинара посвященное Всемирному Дню Логики (https://en.wikipedia.org/wiki/World_Logic_Day) |
В 2023 г. мы продолжили традицию семинара (см. Logic Day 2021 и Logic Day 2020)
совместных заседаний с
Математическим Клубом Университета Иннополис (см. Telegram-беседу Logic Day in Innopolis ).
Программа заседания (со ссылками на некоторые материалы):
|
Дата: пятница 20 января 2023 г. | (Ссылки на некоторые материалы см. в колонке слева.) |
| День Проблем 2022 | В 2022 г. ruStep продолжил традицию проведения в канун нового года Дня Проблем (см. "День Проблем 2020" и "День Проблем 2021"). На заседании выступили (1) Аркадий Валентинович Климов (Институт проблем проектирования в микроэлектронике РАН, Москва) Подкласс сетей Петри, допускающих простое распределенное выполнение, (2) Дмитрий Александрович Кондратьев (Институт систем информатики СО РАН, Новосибирск) Парадигмы задания спецификаций программ и конкурс SpecifyThis, (3) Николай Вячеславович Шилов (Университет Иннополис, Иннополис) Так какова же сложность алгоритма Дейкстры назначения укрытий? | Дата: пятница 30 декабря 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентации, ссылки см. в колонке слева.) |
| Юрий Андреевич Кочетов (Институт Математики СО РАН, Новосибирск): Задачи упаковки для двумерных прямоугольных предметов | Аннотация: Рассматриваются широко изветсные задачи упаковки в полосу и в контейнеры для двумерных прямоугольных предметов с возможностью поворачивать предметы на 90 градусов и с запретом на повороты. Будут представлены математические модели частично-целочисленного программирования, алгоритмы кодирования и декодирования решений. Работа матеэвристики Имитации отжига на основе кодировки решений в виде ориентированных деревьев и так называемой Sky-line процедуры будет продемонстрирована на примерах с малым числом предметов, до 100 прямоугольников. | Дата: пятница 16 декабря 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.) |
| Заседание, посвященное памяти Игоря Васильевича Поттосина (1933-2001) | Прошло более 20 лет со дня кончины Игоря Васильевича, 15 декабря уже будет 21 год. На заседании выступил Алексей Недоря с сообщением Вклад И.В. Поттосина в развитие языков и технологии компиляции в России (Личные воспоминания о том, как это было, как Игорь Васильевич повлиял на появлении и развитии языков Модула-2 и Оберон в СССР и России и на развитии технологии компиляции.) Мы также рекомендуем познакомиться с лекцией Андрея Николаевича Терехова "Игорь Васильевич Поттосин" (на "Лекториуме"). | Дата: пятница 9 декабря 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация выступления Алексея Недори.) |
| Дата очередного заседания семинара ruSTEP пересекалась с датами Открытой конференции Института системного программирования РАН. | Еще точнее: дата заседания семинара ruSTEP совпадала с датой проведения секций Технологии анализа, моделирования и трансформации программ, посвященной методам оптимизации в компиляторе, генерации кода, статическому и динамическому анализу программ и др. С программой секции "Технологии анализа, моделирования и трансформации программ" можно познакомиться по ссылке (см. "Второй день") | Дата: пятница 2 декабря 2022 г. | Рабочая (необработанная) запись заседания секции "Технологии анализа, моделирования и трансформации программ" на YouTube-канале ИСП РАН. |
| Сергей Михайлович Старолетов (Алтайский государственный технический университет): Towards Modeling and Verification of Eurobalise Telegram Encoding Algorithm | В докладе представлена статья С.М. Старолетова недавно опубликованная в Transportation Research Procedia (v. 61, 2022, pp. 447-454, https://doi.org/10.1016/j.trpro.2022.01.073).
Аннотация статьи: A eurobalise is designed to broadcast the current state of the railway to a passing train. Such a transmitter is activated with an approaching train and its goal is to dispatch messages called telegrams. In this article, we consider the encoding process of such telegrams. Since the CRC checksum building method is based on operations with polynomials over the Galois field modulo 2, we describe a proven library to work with polynomials. Next, we present the implementation of the encoder in a modeling language according to the open specification and then discuss its verification strategies using the Model Checking method. |
Дата: пятница 18 ноября 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.) |
| Дмитрий Александрович Кондратьев (ИСИ СО РАН, Новосибирск): Автоматизация дедуктивной верификации C-программ без использования инвариантов циклов | В 2020 и 2021 гг. с 3 по 5 ноября наш семинар служил платформой для проведения ежегодного семинара PSSV - Workshop Program Semantics, Specification and Verification (Theory and Applications) - PSSV-2021 и PSSV-2020. Однако в нынешнем году организаторы PSSV решили воздержаться от проведения семинара.
Поэтому в этом году 4 ноября вместо заседаний PSSV мы провели регулярное заседание семинара ruSTEP, но не обычное, а специальное - посвященное памяти одного из основателей PSSV Валерия Александровича Непомнящего (7 августа 1939 - 25 декабря 2021). Заседание 4 ноября 2022 г. состояло из двух частей: сначала Д.А. Кондратьев представил последнюю опубликованную работу Валерия Александровича "Автоматизация дедуктивной верификации C-программ без использования инвариантов циклов" (написанную совместно с Д.А. Кондратьевым), а потом состоялась мемориальная сессия. (Напоминаю, что в 2019 г. в ИСИ СО РАН прошел Коллоквиум по Теоретическому и Экспериментальному Программированию посвященный юбилею Валерия Александровича Непомнящего (КолТЭП-2019) Аннотация доклада Д.А. Кондратьева: Автоматизация верификации C-программ ‒ актуальная проблема современного программирования. Для ее решения необходимо автоматизировать решение проблемы инвариантов циклов, доказательство условий корректности и локализацию ошибок в случае ложных условий корректности. В Институте систем информатики СО РАН разрабатывается система C-lightVer, использующая комплексный подход к автоматизированной дедуктивной верификации C-программ. Данный подход включает символический метод верификации финитных итераций для элиминации инвариантов циклов, стратегии доказательства условий корректности и метод локализации ошибок. Символический метод верификации финитных итераций основан на замене действий циклов определенного вида применением специальной рекурсивной функции rep. Метод локализации ошибок основан на сопоставлении условий корректности с исходным кодом и генерации текста о соответствии условий корректности и фрагментов программы. Естественно возникает задача автоматизации верификации C-программ с вложенными циклами. Применение символического метода верификации финитных итераций для таких программ приводит к композиции функций rep для внешнего и вложенного циклов. Новым результатом, представленным в данном докладе, является стратегия автоматизации доказательства таких условий корректности. Данная стратегия основана на индукции по номеру итерации внешнего цикла. Для доказательcтва шага индукции мы используем другой результат, представленный в данном докладе, которым является стратегия для программ, спецификации которых содержат функции со свойством конкатенации. В данном докладе также представлены стратегии локализации ошибок и модификация метода локализации ошибок для случая вложенных циклов. Эти стратегии используются для проверки выполнения свойств циклов, которые могут означать наличие ошибок. В качестве примера применения наших результатов рассматривается автоматическая верификация сортировки простыми вставками без инвариантов циклов. Библиографическая ссылка: Кондратьев Д.А., Непомнящий В.А. Автоматизация дедуктивной верификации C-программ без использования инвариантов циклов // Программирование. 2022. № 5. С. 37-53. |
Дата: пятница 4 ноября 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентации доклада Д.А. Кондратьева, сообщения Н.В. Шилова, а также фотографии В.А. Непомнящего во время семинара PSSV-2018 (предоставлена В. Сазоновым и М. Трахтенбротом) и во время конференции PSI-2011 (предоставлена М. Трахтенбротом).) |
| Николай Вячеславович Шилов (Университет Иннополис): Обзр Matching Logic | Был представлен реферат статьи Григори Росу Matching logic (Logical Methods in Computer Science, т. 13, стр. 1-61, декабрь 2017, статья доступна по
ссылке). Данный реферат можно считать продолжением/дополнением к докладу Васила Дядова Формальная операционная семантика в промышленной разработке (на примере K-framework) 23 июня 2022 г.
Аннотация статьи: This paper presents ''matching logic'', a first-order logic (FOL) variant for specifying and reasoning about structure by means of patterns and pattern matching. Its sentences, the ''patterns'', are constructed using ''variables'', ''symbols'', ''connectives'' and ''quantifiers'', but no difference is made between function and predicate symbols. In models, a pattern evaluates into a power-set domain (the set of values that ''match'' it), in contrast to FOL where functions and predicates map into a regular domain. Matching logic uniformly generalizes several logical frameworks important for program analysis, such as: propositional logic, algebraic specification, FOL with equality, modal logic, and separation logic. Patterns can specify separation requirements at any level in any program configuration, not only in the heaps or stores, without any special logical constructs for that: the very nature of pattern matching is that if two structures are matched as part of a pattern, then they can only be spatially separated. Like FOL, matching logic can also be translated into pure predicate logic with equality, at the same time admitting its own sound and complete proof system. A practical aspect of matching logic is that FOL reasoning with equality remains sound, so off-the-shelf provers and SMT solvers can be used for matching logic reasoning. Matching logic is particularly well-suited for reasoning about programs in programming languages that have an operational semantics, but it is not limited to this. |
Даты: пятница 21 и 28 октября, вторник 1 ноября 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН: первая часть, вторая часть и третья часть. ( Есть презентация доклада.) |
| Игорь Алексеевич Адамович (Институт программных систем им. А. К. Айламазяна РАН): Специализация интерпретаторов, написанных на объектно-ориентированных языках, может быть эффективной | Аннотация:
В докладе рассматривается специализация программ на языке Java. Барьеры на пути специализации реальных программ,
написанных в объектно-ориентированной парадигме, часто могут быть преодолены при помощи современных методов метавычислений.
Один из барьеров — необходимость разрешения полиморфизма на этапе анализа программы, до ее исполнения.
Эта проблема успешно решается для ряда случаев в специализаторе JaSpe, что что будет показано в данном докладе.
Помимо прочего, в докладе рассмотрена компиляции программ с использованием метода специализации, без использования компилятора. Мы применили специализатор JaSpe, основанный на методе частичных вычислений, к двум интерпретаторам языка арифметических выражений, написанным на Java. Интерпретаторы были реализованы методом рекурсивного спуска и с использованием шаблона «посетитель». В результате успешной специализации данных интерпретаторов по программе вычисления квадратного корня на языке арифметических выражений были получены скомпилированные версии программы на языке Java. При этом скорость полученных версий программы по сравнению с исходной увеличилась в 12-22 раза. |
Дата: суббота 8 октября 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.) |
| Сирожиддин Зайнитдин угли Комолов (Университет Иннополис): The state of the contemporary science in Uzbekistan | Сирожиддин Комолов — старший преподаватель Университета Иннополис. Недавно он (совместно с Шерзодом Рахматовым) издал в Узбекистане монографический учебник (на узбекском языке) "Основы искусственного интеллекта. Машинное обучение". | Дата: пятница 7 октября 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.) |
| Владимир Владимирович Иванов (Университет Иннополис): Методы анализа сложности текста на русском языке | Аннотация: Автоматическая оценка сложности текстов востребована в образовании и целом ряде других областей. Решение этой проблемы поможет в повышении качества учебных материалов и особенно актуально в свете персонализации обучения. Однако она остается нерешенной даже для английского языка, хотя и привлекала внимание многих исследователей. В докладе будут рассмотрены общие подходы, простые модели расчета сложности текстов на русском языке на основе небольшого числа низкоуровневых параметров, а также нейросетевые модели для задач оценки сложности текста, отдельных предложений и слов. Применительно к русскому языку все перечисленные задачи до сих пор не решались. | Дата: четверг 22 сентября 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН: первая часть, вторая часть и третья часть (и дискуссия). ( Есть презентация доклада.) |
| Карраскель Гомес Хулио Сесар (Высшая Школа Экономики, Москва): Формальное построение и валидация поведения торговых систем с акциями: подход на основе сетей Петри | Аннотация: Доклад представляет результаты Диссертации, защита которой назначена на 16 сентября 2022 г. В докладе представлены исследования по формальному моделированию процессов в торговых системах с использованием различных расширений сетей Петри - известного формализма для моделирования и анализа параллельных распределенных систем. Сначала рассказано, что такое торговые системы и process mining (дисциплина науки о данных, которая фокусируется на анализе процессов). Потом объяснен выбор вариаций сетей Петри для проверки соответствия процессов в торговых системах и представим полученные результаты. | Дата: четверг 8 сентября 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН: первая часть и вторая часть. ( Есть презентация доклада.) |
| Николай Дмитриевич Кудасов (Университет Иннополис, Россия): Higher-order unification from E-unification with second-order equations and parametrised metavariables | Аннотация: Type checking and, to a larger extent, type and term inference in programming languages and proof assistants can be implemented by means of unification. In presence of dependent types, variations of higher-order unification are often used, such as higher-order pattern unification. In practice, there are often several mechanisms for abstraction and application, as well as other eliminators (such as projections from pairs) that have to be accounted for in the implementation of higher-order unification for a particular language. In this work, we study the possibility of representing various higher-order unification problems as a special case of E-unification for second-order algebra of terms. This allows us to present beta-reduction rules for various application terms, and some other eliminators as equations, and reformulate higher-order unification problems as E-unification problems with second-order equations. We then present a procedure for deciding such problems, introducing second-order mutate rule (inspired by one-sided paramodulation) and generic versions of imitate and project rules. We also provide a prototype Haskell implementation for syntax-generic higher-order unification based on these ideas in Haskell programming language. | Дата: четверг 30 июня 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН: первая часть, вторая часть, третья часть и четвертая часть. ( Есть презентация доклада.) |
| Васил Дядов(Лаборатория Касперского, Москва): Формальная операционная семантика в промышленной разработке (на примере K-framework) | Аннотация: K-framework — это современный подход к проектированию языков программирования, анализу и верификации программ. Он позволяет простым и интуитивно понятным образом определить операционную семантику языка программирования и автоматически получить набор инструментов: от интерпретаторов до машин символьного исполнения и доказательства корректности. Можно буквально за 15 минут сконструировать свой язык и начать программировать на этом языке, экспериментировать, тестировать, доказывать свойства программ и так далее. В настоящее время K-framework все шире используется в промышленности: от блокчейнов до аэрокосмических программ NASA. И на практике было показано, что это очень эффективный инструмент для верификации программ, свойств безопасности и анализа защищенности. Также K-framework очень полезен в курсах информатики, которые нацелены на дизайн языков и формальную семантику. | Дата: четверг 23 июня 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация и дискуссия в чате.) |
| Артем Станиславович Андросов и Сергей Петрович Шарый(Новосибирский Государственный Университет): IntvalPy - библиотека интервальных вычислений на языке Python | Аннотация: В докладе рассматривается библиотека IntvalPy, реализующая интервальные вычисления на языке Python. В отличие от других существующих интервальных библиотек IntvalPy предоставляет возможность работы как с классической интервальной арифметикой, так и с полной интервальной арифметикой Каухера. Кроме того, библиотека была разработана с учётом стандарта IEEE 1788-2015 на интервальные вычисления на ЭВМ, что гарантирует высокую точность результатов. Верхнеуровневая функциональность библиотеки IntvalPy реализует новейшие методы для распознавания и оценивания множеств решений интервальных линейных систем уравнений, вычисления их формальных решений, а также визуализации множеств решений интервальных уравнений и систем уравнений. | Дата: четверг 16 июня 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.) |
| Андрей Андреевич Белеванцев (Институт системного программирования РАН): Алгоритмы статического анализа инструмента Svace | Аннотация: Аннотация: В докладе представлено современное состояние статического анализатора Svace, разрабатываемого в Институте системного программирования им. Иванникова РАН. Svace ищет ошибки в программах на языках С/С++, Java, Kotlin, Go и C#. Будет дано краткое описание анализатора, после чего представлены основные алгоритмы внутрипроцедурного анализа потока данных, основанные на идентификаторах значений, межпроцедурного анализа на основе резюме, статического символьного выполнения, вспомогательные алгоритмы анализа. Также будут обсуждены особенности анализа языков, отличных от С. | Даты: четверг 26 мая и четверг 2 июня 2022 г. | Первая часть доклада состоялась 26 мая 2022 г. (рабочая запись на YouTube-канале ИСИ СО РАН), вторая - 2 июня 2022 г. (рабочая запись на YouTube-канале ИСИ СО РАН). |
| Виолетта Сим (Университет Иннополис, Россия): Formalizing ɸ-calculus: a purely object-oriented calculus of decorated objects | Аннотация: Many calculi exist for modelling various features of object-oriented
languages. Many of them are based on λ-calculus and focus either
on statically typed class-based languages or dynamic prototypebased languages. We formalize untyped calculus of decorated objects, informally presented by Bugayenko, which is defined in terms
of objects and relies on decoration as a primary mechanism of object extension. It is not based on λ-calculus, yet with only four
basic syntactic constructions is just as complete (in particular, it is
Turing complete and possesses Church-Rosser property). We also
provide a sound translation to Wand’s λ-calculus with records and
concatenation, and discuss the key differences of these calculi.
Исследование выполнено совместно с Н.Д. Кудасовым. |
Дата: среда 1 июня 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть дискуссия в чате..) |
| Кирилл Викторович Зиборов (Московский государственный университет): Формальная верификации смарт-контрактов, разработанных для СРР InnoChain | Аннотация: В докладе была представлена математическая модель исполнения смарт-контрактов, учитывающая понятие состояния и его изменение в системе распределенного реестра. Данная модель реализована в среде интерактивного доказательства теорем HOL4, а также продемонстрирована возможность её применения для спецификации свойств корректности смарт-контрактов. Также рассмотрены два подхода к разработке моделей смарт-контрактов в HOL4 и проведено их сравнение. Первый подход использует только функции высших порядков, а второй опирается на понятие монады и монадических функций. Предложенная модель исполнения смарт-контрактов и подходы для моделирования логики их работы были применены для реализации и формальной верификации смарт-контракта, управляющего заправкой воздушных судов. На данном примере показано, что на практике модели смарт-контрактов из HOL4 могут быть транслированы и интегрированы с исходным кодом системы распределенного реестра InnoChain на языке программирования CakeML. Репозиторий материалов проекта доступен по ссылке https://github.com/RZRussel/hol4-contract-verification. | Дата: четверг 12 мая 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.) |
| Игорь Сергеевич Ануреев (ИСИ СО РАН и Cyber-Physical Systems Lab, Новосибирск): Онтологический подход к дедуктивной верификации императивных программ | Аннотация: В докладе представлен онтологический подход к дедуктивной верификации императивных программ. Основой подхода являются новый вид систем переходов - атрибутные системы, язык спецификации атрибутных систем ASL и новые виды семантик императивных языков программирования - онтологическая, онтологическая операционная и онтологическая логическая. Подход проиллюстрирован на модельном императивном языке. | Дата: четверг 10 февраля (первая часть) и 28 апреля (вторая часть) 2022 г. | Рабочая (необработанная) запись первой части доклада на YouTube-канале ИСИ СО РАН. |
| Наталья Олеговна Гаранина (ИСИ СО РАН и Cyber-Physical Systems Lab, Новосибирск): Формальные аспекты темпоральной логики, управляемой событиями | Аннотация: В докладе представлен формализм Event-Driven Temporal Logic (EDTL) для спецификации требований к реактивному программному обеспечению. EDTL-требования представляются как 6-ти компонентный шаблон, связывающий появление и последовательность наблюдаемых событий параллельной системы. Формальная семантика EDTL-требований представлена в виде конечного автомата, LTL-формулы и FOL-формулы. Разработаны методы ограниченной верификации для EDTL-требований, проверки непротиворечивости набора EDTL-требований, формальная семантическая классификация EDTL-требований и способ представления некоторых классов EDTL-требований на естественном языке. Есть идея алгоритма проверки моделей для EDTL-требований. | Дата: четверг 14 апреля 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.) |
| Николай Вячеславович Шилов (Университет Иннополис): "Computer science and its relation to mathematics" - статья Дональда Кнута, изменившая мою жизнь. Обзор статьи, некоторые воспоминания и размышления спустя 44 года после первого знакомства с ней. | Кратное описание: 1 апреля отмечается в Новосибирском государственном университете и во многих университетах мира как День Математика. Поэтому на специальном заседании семинара, посвященном Дню Математика, Н.В. Шилов сделал обзор статьи Д. Кнута Computer science and its relation to mathematics by Donald Knuth (1974, Amer. Math. Monthly., 81(4), doi:10.2307/2318994б с которой впервые познакомился в 1977 г. | Дата: пятница 1 апреля 2022 г. | |
| Мария Сергеевна Ушакова (Сибирский Федеральный Университет, Красноярск): Формальная верификация функционально-потоковых параллельных программ | Аннотация: Доклад посвящен использованию методов формальной верификации для программ, разрабатываемых на языке Пифагор. Лежащая в основе языка функционально-потоковая модель параллельных вычислений позволяет представлять программу в виде информационного графа, не связанного ресурсными ограничениями. Это позволяет при формальной верификации ориентироваться только на логику информационных зависимостей программы, упрощая тем самым процесс анализа. В рамках проделанных исследований для функционально-потоковых параллельных программ разработан метод формальной верификации, основанный на исчислении Хоара. Для повышения наглядности при проведении доказательства используется визуальное представление информационного графа программы.
Также для лучшего понимания функционально-потоковой парадигмы параллельного программирования в докладе будет кратко охарактеризован весь проект Пифагор.
Доклад представляет материалам и результаты кандидатской диссертации по специальности 2.3.5. - Математическое и программное обеспечение вычислительных систем, комплексов и компьютерных сетей (технические науки). С текстом диссертации и авторефератом можно познакомиться по ссылке https://research.sfu-kras.ru/node/14728. |
Дата: четверг 17 марта 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация и дискуссия в чатеt.) |
| Специальное заседание в Международный женский день | Как и год назад ruSTEP провел специальное заседание в Международный женский день с двумя докладами.
|
Дата: вторник 8 марта 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентации докладов Л.В. Городней и Д.А. Кондратьева, И.В. Шошминой, а также запись чата семинара.) |
| Radhakrishnan Delhibabu (School of Computer Science and Engineering Vellore Institute of Technology (VIT), Веллор, Индия): Application of Artificial Intelligence | Кратное описание: В докладе проф. Radhakrishnan Delhibabu представил свои исследования в области искусственного интеллекта. | Дата: среда 16 февраля 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.) |
| Татьяна Валентиновна Снытникова: Эффективная реализация модели ассоциативных вычислений на графических ускорителях | Аннотация: В докладе была представлена реализация модели ассоциативных вычислений (STAR-машина) на графических ускорителях. Обоснована эффективность этой реализации: реализация на GPU обладает ассоциативными свойствами в слабом смысле. Это подтверждается как теоретическими оценками, так и вычислительным экспериментом. Далее приводятся рекомендации по адаптации и оптимизации ассоциативных алгоритмов под выполнение на GPU. На графе с 5000 вершин адаптированный под GPU ассоциативный алгоритм транзитивного замыкания графа выполняется быстрее в 2378 раз по сравнению с последовательным алгоритмом. В докладе были представлены материалам и результаты кандидатской диссертации по специальности 05.13.11 - математическое и программное обеспечение вычислительных машин, комплексов и компьютерных сетей. | Дата: четверг 3 февраля 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация и дискуссия в чате.) |
| Встреча по случаю World Logic Day (https://en.wikipedia.org/wiki/World_Logic_Day) |
Краткое описание: В этом году наш семинар продолжил традицию встреч, посвященных "Всемирному Дню Логики", начатую год назад.
Встреча прошла как совместно с
Математическим Клубом Университета Иннополис (см. также специальный чат Logic Day in Innopolis).
Программа (вместе со ссылками на материалы некоторых выступлений):
|
Дата: пятница 28 января 2022 г. | (Ссылки на некоторые материалы см. в колонке слева.) |
| Иван Глазунов и Константин Дьяченко (основатели компании Deep Foundation): Ассоциативные модели данных и наследие идей Саймона Вильямса и Эдгара Кодда. Проект Deep.Foundation | Аннотация (предоставлена авторами): Проект Deep.Foundation - это сквозная архитектура для производства совместимых IT решений, ассоциативное хранилище как метаязык, интерфейс для пространственного восприятия данных, единая информационная теория всего. | Дата: Четверг 27 января 2022 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть предварительный вариант презентации доклада и дискуссия в чате.) |
| Андрей Валентинович Климов (Институт прикладной математики им. М.В. Келдыша РАН, Москва, Россия): Почему частичные вычисления и суперкомпиляция до сих пор широко не используются на практике? Размышления в свете российских работ по метавычислениям | Аннотация: Проблема оказалась труднее, чем мечталось отцам-основателям этого научного направления — Валентину Турчину, Андрею Ершову и, наверно, Ёcихико Футамуре и Нилу Джоунсу тоже. «Великого оптимизатора программ», работающего нажатием кнопки, не получилось. Тем не менее, подходы к построению систем метавычислений, полезных на практике, существуют, только до сих пор им не уделялось достаточного внимания. Отбросив надежды на легкость задачи, обсудим, как быть дальше. В качестве материала для выводов используем российский опыт работ по суперкомпиляции и частичным вычислениям и лишь укажем на западные работы, наиболее значимые для нас, поскольку из опубликованных чужих работ трудно извлечь нужный нам отрицательный опыт, так как обычно такие результаты не публикуется, в то время как про свои работы мы знаем, куда стремились, что получилось и где споткнулись.
Это выступение является предварительной версией пригашеннго доклада 17 января 2022 на PEPM'22. |
Дата: четверг 13 января 2022. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада и дискуссия в чате.) |
| День Проблем | В 2021 г. ruStep продолжил традицию, начатую в 2020 г., провел в канун нового года "День Проблем", на котором выступили (1) Андрей Валентинович Климов (Институт прикладной математики РАН, Москва) Теории имен А. Питтса и М. Габбая и семантика ссылок в языках программирования, (2) Аркадий Валентинович Климов (Институт проблем проектирования в микроэлектронике РАН, Москва) О моделировании машин Тьюринга сетями Петри, (3) Дмитрий Александрович Кондратьев (Институт систем информатики СО РАН, Новосибирск) Небольшая программа, демонстрирующая сложности автоматизации дедуктивной верификации, (4) Борис Леонидович Файфель (Саратовский государственный технический университет) Вычисление чисел Фибоначчи по формуле Бине без использования плавающей арифметики, (5) Николай Вячеславович Шилов (Университет Иннополис, Иннополис) Как "встроить" программную инженерию в курсы по математике для программистов? | Дата: четверг 30 декабря 2021 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентации (ссылки см. в колонке слева) и дискуссия в чате.) |
| Виталий Анатольевич Романов (Университет Иннополис): Type Prediction in Source Code with Graph Neural Network Embeddings | Аннотация: Current state-of-the-art results for source code analysis with Neural Networks are achieved using famous Transformer architecture. One example of pre-trained model for source code is CodeBERT. Graph Neural Networks (GNNs) provide an alternative technique for pre-training source code embeddings. However, the strengths and weaknesses of GNN embeddings are not well studied on downstream tasks. In this work, we consider the problem of pre-training GNN embeddings for source code. We evaluate pre-trained embeddings using the task of variable type prediction for dynamically typed programming language Python. Our experiments show that GNN embeddings pre-trained with Name Prediction objective achieve performance comparable to CodeBERT embeddings. Moreover, combining CodeBERT and GNN embeddings into a Hybrid Type Prediction model allows to further improve type prediction accuracy by more than 10%. These improvements are achieved just after training GNN embeddings for one epoch – a fraction of time that is needed to pre-train CodeBERT embeddings. | Дата: четверг 23 декабря 2021. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Владислав Александрович Перепёлкин (Институт вычислительной математики и математической геофизики СО РАН, Новосибирск): Язык и система LuNA автоматического конструирования параллельных программ численного моделирования на мультикомпьютерах | Аннотация: Система LuNA позволяет автоматически конструировать и исполнять на мультикомпьютерах параллельные программы численного моделирования на основе высокоуровневой спецификации программы на одноимённом языке. LuNA-программа представляет собой описание множества фрагментов данных и вычислений, что позволяет системе автоматически планировать и реализовывать вычисления распределённо, динамически балансировать нагрузку на вычислительные узлы, осуществлять необходимые коммуникации между узлами и выполнять ряд других низкоуровневых задач параллельного программирования, освобождая от этой работы пользователя. В докладе представляются язык описания прикладных алгоритмов, ключевые системные алгоритмы, осуществляющие его трансляцию и распределённое исполнение, а также представлены система LuNA и результаты её экспериментального исследования. | Дата: четверг 16 декабря 2021. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада и дискуссия в чате.) |
| Александр Когтенков (Технологический институт Шаффхаузена, Швейцария): A sound formalization of void safety | Аннотация: One of the principal source of program crashes and security attacks is the null-pointer (or void-reference) dereferencing, which results from an attempt to use a non-existing object. Mainstream languages, object-oriented or not, are subject to this risk. A number of languages, most notably Eiffel, pioneered "void-safety", which provides a guarantee that no such events will occur. Formal proofs are required, however, to guarantee the soundness of such schemes. This talk examines one of the published approaches, "Freedom before commitment" by Summers and Müller, shows through a formalization in Isabelle/HOL that it contains errors, and corrects them. | Дата: четверг 2 декабря 2021. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАНl. (Есть презентация доклада.)) |
| Swati Megha (Университет Иннополис): Design Patterns Detection Using Machine Learning Model | Аннотация: Design patterns are used to address common design problems in software systems. Several Machine learning models have been proposed for detecting and recommending design patterns for a software system. However, lesser research is done on using Machine learning models for establishing a correlation between design patterns and code quality. In this paper, firstly, we created a data set of 378 open-source software projects primarily from GitHub and GitLab to train models. Secondly, we compared several pattern detection machine learning models based on the most popular classifier families for three categories of design patterns, namely Creational, Structural, and Behavioral. We then compared five standard performance matrix namely, Precision, Recall, Accuracy, and FI-Score for eight different classifier families. The proposed model showed noticeable improvement in Precision and Accuracy, while the identified improvements in Recall and FI-Score were moderate. | Дата: четверг 25 ноября 2021. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| XII Workshop on Program Semantics, Specification, and Verification
Список приглашенных докладчиков:
|
Традиция ежегодных семинаров PSSV была заложена в 2010 г. Валерием Александровичем Непомнящим (Институт систем информатики СО РАН) и Валерием Анатольевичем Соколовым (Ярославский государственный университет).
В 2021 г. семинар организовывала Лабораторией программной инженерии Университета Иннополис и прошла онлайн 4-5 ноября 2021 г. (в Zoom). |
Даты: четверг 4 ноября и пятница 5 ноября 2021 г. | Прграмма семинара PSSV-2021 (со ссылками на видиозаписи и аннотации докладов) дспупна поседующей ссыке. |
| Рене ван Беверн (Новосибирский государственный университет): Рандомизированные алгоритмы. Как жить с вероятностью ошибки. | Заседание прошло под эгидой
Computer Science Center.
Анно тация: В информатике методы теории вероятностей встречаются в различных видах. В лекции мы рассмтрели для чего можно выгодно использовать случайность при построении алгоритмов и познакмиись с примерами, которые демонстрируют общее свойство многих рандомизированных алгоритмов: они часто простые, порой даже такие простые, что до них сложно додуматься. С другой стороны было показано, что простота этих алгоритмов часто обусловлена их нетривиальным анализом: более сложные алгоритмы было бы слишком сложно анализировать. |
Дата: четверг 21 октября 2021. | Рабочая (необработанная) запись на YouTube-канале Computer Science Center. |
| Николай Вячеславович Шилов (Университет Иннополис): Эксперименты с вариантами Исчисления Алиасв для модельного процедурного языка программирования с разрешимой адресной арифметикой | Аннотация: Исчисление алиасв было предложено Бертраном Мейером в 2011 году для модельного языка программирования с одним типом данных (для указателей). Это исходное исчисление представляет собой формализм, основанный на множествах, представленный как набор управляемых синтаксисом правил, как вычислять аппроксимацию aft(S,P) для наложения аиасов после выполнения программы P для данного начального псевдонима S. В 2014 году Н.В. Шилов, А. Атекбаева и А. Воронцов предложили исчисление алиасов для более реалистичного (но все же модельного) процедурного языка программирования MoRe с адресуемой памятью.
В докладе было рассказано о реализации прототипа инструмента анализа алиасов для MoRe. Инструмент основан на новой облегченной версии исчисления псевдонимов, предназначенной для анализа утечки памяти. Он был протестирован с использованием нескольких коротких фрагментов кода MoRe, содержащих различные ошибки утечки памяти, и продемонстрировал свою правильность (путем обнаружения этих ошибок).
(По материалам совместной работы с Леонидом Ильичем Лыгиным.) |
Дата: четверг 7 октября 2021. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Дмитрий Александрович Кондратьев (ИСИ СО РАН): Автоматизированная локализация ошибок в С-программах с помощью дедуктивной верификации | Аннотация: Система C-lightVer разрабатывается в Институте систем информатики им. А.П. Ершова СО РАН. Это система для автоматической дедуктивной верификации C-программ. Проблема автоматизации дедуктивной верификации включает задачу локализации ошибок. Классическая дедуктивная верификация приводит к недоказанным или ложным условиям корректности в случае наличия ошибок во входной программе. Пользователь системы верификации нуждается в подробных объяснениях недоказанных или ложных условий корректности. Значительная модификация метода семантической разметки была реализована в системе C-lightVer для решения данной проблемы. Исходный метод основан на снабжении подформул условий корректности семантическими метками. Семантическая метка хранит информацию о соответствии между подформулой условия корректности и исходным кодом программы. Данная информация конвертируется в текст на естественном языке. Объяснение условия корректности получается из объединения текстов, сгенерированных для каждой семантической метки. Расширение метода семантической разметки, реализованное в системе C-lightVer, позволяет пользователю использовать не только семантические метки из стандартного набора, но и самому задавать новые виды семантических меток. Другое расширение позволяет генерировать объяснения в случае входных программ с такими видами циклов, как финитные итерации над структурами данных. Символический метод верификации финитных итераций позволяет избежать задания инвариантов в случае таких циклов. Данный метод основан на символической замене таких циклов на специальные рекурсивные функции. Но полученные условия корректности содержат применения таких рекурсивных функций. Расширение метода семантической разметки позволяет снабдить определения таких функций специальными семантическими метками. Полученное объяснение содержит текст о соответствии между финитной итераций и определением такой функции. | Даты: четверг 23 и 30 сентября 2021 г. | Первая часть доклада состоялась 23 сентября 2021 г. (рабочая запись на YouTube-канале ИСИ СО РАН), вторая - 30 сентября 2021 г. (рабочая запись на YouTube-канале ИСИ СО РАН). (Есть презентация доклада.) |
| Антон Алексеевич Завьялов (Новосибирский государственный университет): Проектирование визуального функционального языка с возможностями оптимизации рекурсии | Аннотация: В докладе рассказано о проектировании и разработке интегрированной среды программирования на визуальном функциональном языке с возможностью оптимизации рекурсии. Рассмотрены вопросы: (i) проектирование визуального языка функционального программирования, (ii)проектирование и разработка интегрированной среды визуального программирования на ранее спроектированном языке, (iii)проектирование и разработка оптимизирующего компилятора программ на ранее спроектированном языке с транслятором в код на языке JavaScript в качестве целевой платформы. | Дата: четверг 9 сентября 2021. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада и чат семинара.) |
| Антонина Николаевна Непейвода (Институт программных систем им. А.К. Айламазяна РАН, г. Переславль-Залеский): Опыты по суперкомпиляции языка Рефал | Аннотация: Это выступление продолжает доклад Александра Владимировича Коновалова по языку Рефал на семинаре ruSTEP 11 июня 2021 г. Будет кратко рассмотрен метод суперкомпиляции в применении к этому языку, и некоторые его приложения. С одной стороны, ассоциативность встроенных данных Рефала усложняет разработку алгоритмов анализа его программ, с другой - даёт возможность доказывать свойства, естественно извлекаемые из программ, записанных на Рефале, и гибко описывать модели структур, обладающих ассоциативностью. В частности, мы покажем, как методами суперкомпиляции моделируются некоторые алгоритмы решения уравнений в словах. | Дата: пятница 9 июля 2021. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Joseph Alexander Brown (Head of the Lab of Artificial Intelligence in Game Development, Innopolis University, Russia): Affordance Theory in Game Design - A Guide Toward Understanding Players | A monograph Affordance Theory in Game Design. A Guide Toward Understanding Players by
Hamna Aslam (Innopolis University) and Joseph Alexander Brown
was published in 2020 by Morgan & Claypool Publishers.
Abstract: Games, whether educational or recreational, are meant to be fun. How do we ensure that the game delivers its intent? The answer to this question is playtesting. However, a haphazard playtest process cannot discover play experience from various dimensions. Players' perceptions, affordances, age, gender, culture, and many more human factors influence play experience. A playtest requires an intensive experimental process and scientific protocols to ensure that the outcomes seen are reliable for the designer. Playtesting and players' affordances are the focus of this book. This book is not just about the playtest procedures but also demonstrates how they lead to the conclusions obtained when considering data sets. The playtest process or playtest stories differ according to the hypothesis under investigation. We cover examples of playtesting to identify the impact of human factors, such as age and gender, to examine a player's preferences for game objects' design and colors. The book details topics to reflect on possible emotional outcomes of the player at the early stages of game design as well as the methodology for presenting questions to players in such a way as to elicit authentic feedback. This book is intended mainly for game designers, researchers, and developers. However, it provides a general understanding of affordances and human factors that can be informative for readers working in any domain. Please follow the links for the table of contents and authors' information. |
Дата: пятница 25 июня 2021. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Александр Владимирович Коновалов (Московский государственный технический университет): Введение в язык Рефал | Аннотация: В докладе рассказано о языке программирования Рефал — история, синтаксис, семантика и основы метавычислений над ним. Показаны основные отличия Рефала (самого языка и метавычислений над ним) от других функциональных языков (в докладе Рефал сравнивался с Хаскелем и Эрлангом). Цель — предварить (предполагаемые в июле-августе) доклады про особенности суперкомпиляции Рефала (а участники семинара с предметной областью не знакомы). | Дата: пятница 11 июня 2021. |
Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН.
(Есть презентация доклада.)
Заметки к докладу, подготовленные Андреем Валентиновичем Климовым. - Продолжить обсуждение можно присоединившись к дискуссионной (Google-) группе нашего семинара. |
Пленарные доклады XI SYRCoSE:
|
SYRCoSE
(Spring/Summer Young Researchers' Colloquium on Software Engineering)
организуется ежегодно начиная с 2007 широко известными специалистами в программной инженерии и программировании Александром Константиновичем Петренко (Институт системного программирования РАН, Москва) и Андреем Николаевичем Тереховым (Санкт-Петербургский Государственный Университет).
В 2021 г. местом проведения коллоквиума стал Национальный исследовательский университет Высшая школа экономики. Коллоквиум состоялся 27-28 мая и прошел в смешанном формате в комплексе ВШЭ на Покровском бульваре и дистанционно в Zoom. С аннотациями пленарных докладов можно познакомиться по данной ссылке. |
Даты выступлений пленарных докладчиков:
|
Записи всех выступлений на SYRCoSE-2021 предоставлены Институтом системного программирования им. В.П. Иванникова РАН и доступны в следующих репозиториях: |
| Артем Сергеевич Бурмяков (Университет Иннополис): Введение в проблему консенсуса и ее применение для разработки неблокирующих параллельных алгоритмов | Аннотация: Проблема консенсуса - это фундаментальная теоретическая проблема для распределенного и параллельного программирования. Проблема имеет огромное влияние на различные области приложений, такие как разработка неблокирующих параллельных алгоритмов, систем блокчейнов, алгоритмов синхронизации времени в распределенных системах и параллельных систем с отказами. В докладе формализована проблема консенсуса и рассмотрены доступные решения. В частности, мы продемонстрировано применение проблемы консенсуса для сравнения мощности синхронизации различных параллельных структур данных (например, очереди FIFO) и примитивов синхронизации ЦП для разработки параллельных неблокирующих алгоритмов с помощью "consensus numbers". | Дата: пятница 14 мая 2021. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Дмитрий Владимирович Кознов (Санкт-Петербургский Государственный Университет и JetBrains): Визуальное моделирование при разработке семейства телекоммуникационных систем | Аннотация: Визуальное моделирование (модельно-ориентированный подход) долгие годы был предметом активных исследований и интереса со стороны индустрии. Вершиной популярности подхода стало создание и продвижение языка UML. Однако к настоящему времени энтузиазм исследователей и практиков к этой теме остыл в связи с отсутствием ощутимых, значимых практических результатов.
В докладе выдвигается тезис о том, что визуальное моделирование может быть успешным, во-первых, в рамках предметно-ориентированного подхода, во-вторых, при бесшовной интеграции со средствами разработки (IDEs), в-третьих, при использовании в рамках разработки семейств систем. В подтверждение этих тезисов в докладе описывается пилотное предметно-ориентированное решение для программно-аппаратного семейства телекоммуникационных систем, нацеленного на автоматизацию разработки драйверов к аппаратуре и созданного на основе model-based стека технологий Eclipse. |
Дата: пятница 30 апреля 2021 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. |
| Андрей Михайлович Райгородский (Московский физико-технический институтб Яндекс): Теория графов и ее приложения | Выступление Андрея Михайловича Райгородского было вторым из двух лекций 2021 г. из серии Ершовских лекций по информатике. Серия была основана в 2007 г. Андрем Александровичем Берсом в память о выдающемся ученом в области информатики академике Андрее Петровиче Ершове. (Подробнее - см. XVI Ершовская лекция по информатике.) | Дата: пятница 23 апреля 2021. | Запись лекции доступна в плейлисте Ершовских лекций. |
| Виктор Николаевич Касьянов (ИСИ СО РАН, Новосибирск): Академик Андрей Петрович Ершов и графы в программировании | Выступление В.Н. Касьянова было первым из двух лекций 2021 г. из серии Ершовских лекций по информатике. Серия была основана в 2007 г. Андрем Александровичем Берсом в память о выдающемся ученом в области информатики академике Андрее Петровиче Ершове. (Подробнее - см. XV Ершовская лекция по информатике.) | Дата: пятница 16 апреля 2021. | Запись лекции доступна в плейлисте Ершовских лекций. |
| Первое рабочее совещание (workshop) ''Проект VeriDevOps - концепция, текущая работа'' |
На совещании бала представлена базовая концепция проекта VeriDevOps, цель которого автоматизация защиты и верификации для предотвращения различных угроз кибер-безопасности. Основа проекта формализация требований к кибер-безопасности, верификация и защита.
Проект находится на начальной стадии, поэтому в докладах были представлены базовые идеи и текущие направления разработки:
|
Дата: пятница 16 апреля 2021 г. | Запись совещания на YouTube канале Андрея Александровича Садовых. |
| Андрей Александрович Садовых (Университет Иннополис): Хакатоны в программах обучения разработке ПО. Опыт применения. | Аннотация: При обучении разработке ПО мы сталкиваемся с несколькими проблемами: (1) у многих студентов не хватает опыта чтобы понять важность теоритического материала в практическом применении, что ведет к отстуствию мотивации и низкой вовлеченности; (2) программам обучения и исследователям нужен постоянный контакт с индустрией, что трудно реализовать в рамках классических курсов; (3) у компаний затруднен доступ к результатам исследований в области разработки ПО, а так же затруднена возможность донести до преподавателей и студентов насущные проблемы разработки. Мы предлагаем обучающие хакатоны, как способ улучшить образовательный и иследовательский процесс с помощью кратковременных но интенсивных встреч где компании, исследователи и студенты вместе решают небольшие задачи из индустрии. В докладе обсуждаем один из рецептов проведения хакатона, обобщаем отзовы участников и обсуждаем развитие этой идеи. | Дата: пятница 2 апреля 2021 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Александр Анатольевич Семенов (Институт динамики систем и теории управления, Иркутск): Применение алгоритмов решения SAT к обращению дискретных функций с приложениями в криптоанализе | Аннотация: Доклад предполагает краткий обзор последних достижений в разделе алгебраического криптоанализа, в котором к системам уравнений криптоанализа применяются современные SAT решатели (SAT-based cryptanalysis). Было рассказано об общих техниках трансляции алгоритмов, задающих дискретные функции, в SAT. Будет дано точное понятие SAT иммунности дискретной функции. С использованием этого понятия было показано, как свести к задаче псевдобулевой оптимизации проблему построения атаки из класса «угадывай и определяй» на рассматриваемую функцию. Также были представлены результаты ряда вычислительных экспериментов. | Дата: пятница 19 марта 2021 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Лидия Васильевна Городняя (ИСИ СО РАН, Новосибирск): Не обижайте девушек и женщин! | Доклад Л.В. Городней - основное выступление на "обобщенном 8 марта" - заседании семинара, организованного совместно с
Математическим Клубом Университета Иннополис.
Аннотация: Доклад базируется преимущественно на фактографии вокруг термина "архитектура фон Неймана", конфликта вокруг патента на конструкцию ENIAC-а, особенностях юбилейных мероприятий и истории ЭВМ в нашей стране. Кроме собственно документов отдельные штрихи являются реконструкцией автора, основанной на понимании механизмов поведения. После выступления Л.В. Городней состоялась открытая дискуссия. Участники заранее посмотрели несколько фильмов об женщинах-математиках (например, "Одаренная" и "Скрытые фигуры"). |
Дата: понедельник 8 марта 2021 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Александр Михайлович Дехтярь (Калифорнийский Государственный Политехнический Университет, Сан Луис Обиспо): Координированное преподавания курса "Программная Инженерия для Всех | Аннотация: В наши дни, преподавание основ программной инженерии в высших учебных заведениях фактически эксклюзивно ведется только для студентов "вычислительных" специальностей (информатика, компьютерные науки, программная инженерия, компьютерная инженерия, информационные системы). В то же время, барьер для успешного участия в процессе создания программного обеспечения для профессионалов с "невычеслительным" образованием, в ролях владельца ПО, специалиста в предметной области, конечного пользователя, тестера, менеджера по продукту, и других, неукоснительно снижается. Разработчики ПО сталкиваются с не-разработчиками в процессе создания ПО все чаще и чаще. Получается странная ситуация, когда среди участников проекта разработки ПО, одна группа (программисты-разработчики) обучается программной инженерии и процессу создания ПО во время своего обучения в вузах, а другая группа (все остальные участники процесса) не получают такого образования. В этом докладе мы расскажем о начальной стадии нашей попытки исправить эту ситуацию путем разработки и преподавания курса под названием "Программная инженерия без программирования" для студентов, обучающихся "невычеслительным" специальностям. Для того чтобы преподавание этого курса соответствовало девизу нашего университета "Обучайся созидая!" мы использовали технику координированного преподавания для совместного прочтения этого курса и курса "Введение в программную инженерию" для студентов специальности "программная инженерия". "Координированное преподавание" это разработанный нами в начале 2010х подход к преподаванию двух курсов с одной темой направленных на разные студенческие аудитории, при котором, каждый курс содержит свой собственный набор лекционного материала, но оба класса объединены работой над совместными лабораторными заданиями и проектами. Для студентов курса "Программная инженерия без программирования" возможность прямого общения с разработчиками, и совместной работы над программным обеспечением оказалась весьма полезной. В докладе, мы расскажем о том как построено координированное обучение, как оно было применено к курсу "Программная инженерия без программирования", и об извлеченных из нашего опыта уроках. Соавторы: Бруно да Сильва (кафедра Информатики и Программной Инженерии, Калифорнийский Государственный Политехнический Университет, Сан Луис Обиспо), Аня Гудман (кафедра Химии, Калифорнийский Государственный Политехнический Университет, Сан Луис Обиспо). |
Дата: пятница 5 марта 2021 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. |
| Сергей Михайлович Старолетов (Алтайский государственный технический университет): Model checking games and a genome sequence search | Аннотация: В презентации рассмотрена концепция Model Checking Games для решения алгоритмических задач. Описаны текущие подходы в этой области и осуществлен переход к игре между пользователем и верификатором с целью предоставить решение проблемы, закодированное в системе переходов и формуле LTL с требованием. Показано, как программировать и решать некоторые известные головоломки, используя этот подход. Была рассмотрена проблеме поиска паттерна в последовательности генома и рассказано о реализации метода использования Z-функции поиска подстрок на Promela, построении модели, использования реальных вирусных данных, а затем игра проверки модели с верификатором SPIN. Основываясь на экспериментах, можно сказать, что проблема поиска паттерна с некоторыми отклонениями решается с помощью Swarm Model Checking и метода Hash Compact. | Дата: пятница 19 февраля 2021 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Николай Вячеславович Шилов (Университет Иннополис): Устранение рекурсии в задачах на динамическое программирование | Аннотация: Трансформационный подход к верификации программ был очень популярной темой исследований в первые десятилетия теории программирования. Многие выдающиеся пионеры теории программирования внесли свой вклад в разработку данного направления исследований: Джон Маккарти, Амир Пнуэли, Дональд Кнут... Много интересных примеров трансформационного подхода было тщательно изучено, что привело к методам устранения рекурсии, известным как хвостовая рекурсия и как ко-рекурсия. В данной работе мы подробно исследуем (мы надеемся) новые примеры паттернов устранимой рекурсии, причем, устранение рекурсии основано на трансформациях программ и анализе задач, решаемых этими программами. | Дата: пятница 5 февраля 2021 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Заседание, приуроченное к World Logic Day (https://en.wikipedia.org/wiki/World_Logic_Day) | Выступления: (1) Захар Ягудин (студент 2го курса Университета Иннополис) - "О 0-1 законах для графов и логик", (2) Дмитрий Александрович Кондратьев (ИСИ СО РАН) - "Доказательство в системе ACL2 того, что sqrt(2)не является (рациональным) числом", (3) Борис Леонидович Файфель (Саратовский государственный технический университет) - "Решаем логические задачи на императивном языке программирования", (4) Андрей Валентинович Климов (Институт прикладной математики РАН) - "Использование суперкомпиляции для получения эффективных императивных программ для задачи о расстановке ферзей". | Дата: пятница 15 января 2021 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. |
| День проблем | Выступили: (1) Дмитрий А. Кондратьев (ИСИ СО РАН, Новосибирск), (2) Андрей В. Климов (ИПМ РАН, Москва), (3) Аркадий В. Климов (ИППМ РАН, Москва), (4) Н.В. Шилов (Университет Иннополис), (5) Л.В. Городняя (ИСИ СО РАН, Новосибирск). | Дата: среда 30 декабря 2020 г. | |
| Bertrand Meyer (Politecnico di Milano, Innopolis University, and Eiffel Software): The four PEGS of requirements engineering | Abstarct: Bad software requirements can jeopardize projects., but requirements as commonly practiced remain a weak link in software engineering. What passes for requirements in industry usually consists of a few use cases or user stories, which fail to capture many essential aspects of systems. There is a considerable literature on requirements, including some excellent textbooks, but their lessons are rarely heeded; many projects, in particular, fail to take into account the Jackson-Zave distinction between system and environment. The standard IEEE plan for requirements dates back to 1998 and does not meet the demands of today’s ambitious developments. I will present ongoing work intended to help industry produce more useful requirements. It includes precise definitions of requirements concepts and a standard plan for requirements specifications. The plan contains four books covering the four “PEGS” of requirements engineering: Project, Environment, Goals and System. The talk does not attempt to introduce radical new concepts but rather builds on existing knowledge to define a solid basis for requirements engineering and provide projects with precise and helpful guidelines. | Дата: среда 16 декабря 2020 г. | |
| Станислав Павлович Кикоть (London Metropolitan University): Магистерские программы по информатике в Великобритании. | Дата: среда 2 декабря 2020 г. | ||
| Дмитрий Александрович Кондратьев (ИСИ СО РАН): Методы и средства для формальной верификации Cloud Sisal программ. | Аннотация: В ИСИ СО РАН разрабатывается облачная система параллельного программирования (CPPS). Входным языком CPPS является Cloud Sisal. Это функциональный язык программирования, основанный на циклических выражениях. Главной особенностью CPPS является неявный параллелизм, который достигается с помощью векторизации циклических выражений. В состав CPPS входят подсистемы CSV1 и CSV2 для дедуктивной верификации Cloud Sisal программ. Рассмотрим сходства обеих подсистем. Во-первых, входным аргументом обеих подсистем является Cloud Sisal программа, аннотированная на языке системы ACL2. Во-вторых, для избежания задания инвариантов циклов в обеих подсистемах используется символический метод верификации финитных итераций. Этот метод основан на замене действия цикла на применение рекурсивной функции. В-третьих, в обеих подсистемах для доказательства условий корректности применяется система ACL2. Рассмотрим основное отличие обеих подсистем. Подсистема CSV1 основана на трансляции Cloud Sisal программ в C-программы. К результату трансляции применяется система дедуктивной верификации C-lightVer, разработанная в ИСИ СО РАН ранее. Поэтому, символический метод верификации финитных итераций применяется к циклам языка C, полученным в результате трансляции Cloud Sisal циклов. Система ACL2 применяется для доказательства условий корректности полученных C-программ. В отличие от подсистемы CSV1, подсистема CSV2 основана на дедуктивной верификации исходных Cloud Sisal программ. Поэтому, символический метод верификации финитных итераций применяется к Cloud Sisal циклам. Система ACL2 применяется для доказательства условий корректности исходных Cloud Sisal программ. | Даты: первая часть - среда 18 ноября 2020 г., вторая часть - среда 25 ноября 2020 г. | |
| Александр Владимирович Наумчев (Университет Иннополис): Seamless Requirements and specifications. | Дата: среда 28 октября 2020 г. | ||
| Наталья Олеговна Гаранина (ИСИ СО РАН): An Ontology-based Approach to Support Formal Verification of Concurrent Systems. | Abstract: Formal verification ensures the absence of design errors in a system with respect to system's requirements. This is especially important for the control software of critical systems, ranging from automatic components of avionics and spacecrafts to modules of distributed banking transactions. We present a verification support framework that enables automatic extraction of a concurrent system's requirements from the technical documentation and formal verification of the system design using an external or built-in verification tool that checks whether the system meets the extracted requirements. Our support approach also provides visualization and editing options for both the system model and requirements. The key data components of our framework are ontological descriptions of the verified system and its requirements. We describe the methods used in our support framework and we illustrate their work for the use case of an automatic control system. | Дата: среда 21 октября 2020 г. |