ru-STEP по-русски

 

Российский онлайн-семинар
по фундаментальным вопросам программной инженерии,
теории и экспериментальному программированию:
ru-STEP = russian seminar on Software Engineering, Theory and Experimental Programming.

(Тестовая версия страницы семинара. При необходимости Вы можете перейти на страницу семинара на английском языке.)

Учредители семинара:

  • Игорь Сергеевич Ануреев (Институт систем информатики СО РАН - Новосибирск, anureev "на" iis.nsk.su)
  • Дмитрий Александрович Кондратьев (Институт систем информатики СО РАН - Новосибирск, apple-66 "на" mail.ru)
  • Александр Владимирович Наумчев (Университет Иннополис - Иннополис, a.naumchev "на" innopolis.ru)
  • Денис Константинович Пономарев (Институт систем информатики СО РАН и Новосибирский Государственный Университет - Новосибирск, ponom "на" iis.nsk.su)
  • Алексей Владимирович Промский (Институт систем информатики СО РАН - Новосибирск, promsky "на" iis.nsk.su)
  • Андрей Александрович Садовых (Университет Иннополис - Иннополис, a.sadovykh "на" innopolis.ru)
  • Николай Вячеславович Шилов (Университет Иннополис - Иннополис, shiloviis "на" mail.ru)

Общие сведения о семинаре:

Как зарегистрироваться для участия в семинаре, в обсуждениях и/или как подать заявку на выступление:

  • Желающие выступить на семинаре приглашаются написать по электронной почте любому/нескольким/всем из учредителей семинара (с темой письма "Заявка на ru-STEP").
  • Желающие получать напоминание (оповещение) о ближайшем заседании накануне семинара (тему, докладчика, техническую среду проведения, дату и время) могут заполнить Google-форму https://forms.gle/earZy3hFJKmHQLoZ7.
  • Для обсуждения работы семинара, состоявшихся докладов и других связанных с семинаром тем создана (Google-)группа.

Предстоящие заседания семинара:

Рене ван Беверн (Новосибирский государственный университет): Рандомизированные алгоритмы. Как жить с вероятностью ошибки. Заседание пройдет под эгидой the Computer Science Center.
Внимание: доклад будет сделан на русском языке!
Аннотация: В информатике методы теории вероятностей встречаются в различных видах. В первой части лекции мы посмотрим, для чего можно выгодно использовать случайность при построении алгоритмов. Увидим примеры, которые нам покажут общее свойство многих рандомизированных алгоритмов: они часто простые, порой даже такие простые, что до них сложно додуматься. С другой стороны мы увидим, что простота этих алгоритмов часто обусловлена их нетривиальным анализом: более сложные алгоритмы было бы слишком сложно анализировать. Во второй части лекции мы ознакомимся с двумя главными видами рандомизированных алгоритмов: алгоритмы Монте-Карло и алгоритмы Лас-Вегас. А также поймём, как и какой ценой можно снизить вероятность ошибки и что малой вероятностью ошибки вполне можно пренебречь на фоне других рисков в жизни.
День, дата и время: четверг 21 октября 2021 г. 11:30-13:00 московского /15:30-17:00 новосибирского времени Ссылка на трансляцию в YouTube https://youtu.be/9v5npQUXhyU, во время лекции будет доступен чат, в котором можно будет задавать вопросы.
Рекомендуем пройти регистрацию на https://compscicenter.timepad.ru/event/1810962/ (для своевременного оповещении об изменении ссылки на трансляцию).
Приглашаем на XII Workshop Program Semantics, Specification and Verification: PSSV-2021 На PSSV-2021 будут организованы три специальные сессии:
  • Сессия, посвященная юбилею Александра Константиновича Петренко, заведующего отделом Технологий программирования Института системного программирования РАН (ИСП РАН)
    • А.К. Петренко: Место формальных методов в современном программировании
    • В.В. Кулямин: Формальные модели безопасности
    • А.С. Камкин: Высокоуровневый синтез вычислительных систем: мотивация, проблемы и существующие решения
    • А.В. Хорошилов: Верификация операционных систем
  • Сессия Университета Иннополис
    • Е. Бугаенко: EOLANG и φ-исчисление
    • Н.Д. Кудасов: Nameless and scope-safe (de Bruijn notation as a nested datatype): Sound, Expressive, Fast
    • А.В. Наумчев: The Role of Formalism in System Requirements (- joint work with Jean-Michel Bruel, Sophie Ebersold, Florian Galinier,Manuel Mazzara, Bertrand Meyer)
  • Сессия Института Систем Информатики СО РАН
    • И.С. Ануреев: Онтологический подход к дедуктивной верификации программ
    • Н.О. Гаранина: The Optimization Problem with Model Checking
    • Д.А. Кондратьев: Автоматическая дедуктивная верификация Си программ в системе C-lightVer
Более подробная информация об этих докладах доступна на странице PSSV-2021
Даты: четверг 4 ноября и пятница 5 ноября 2021 г. Программа и расписание будут опубликованы на странице PSSV-2021 не позже понедельника 1 ноября 2021 г.  Объявление о регистрации и канале вещания будут объявлены на странице PSSV-2021 не позже понедельника 1 ноября 2021 г.

Прошедшие заседания семинара: (в порядке Last-In - First-Out):

Николай Вячеславович Шилов (Университет Иннополис): Эксперименты с вариантами Исчисления Алиасв для модельного процедурного языка программирования с разрешимой адресной арифметикой Аннотация: Исчисление алиасв было предложено Бертраном Мейером в 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.
С аннотациями пленарных докладов можно познакомиться по данной ссылке.
Даты выступлений пленарных докладчиков:
  • Д.А. Мордвинов - четверг 27 мая,
  • А.В. Подкопаев - пятница 28 мая,
  • Holger Schlingloff - пятница 28 мая.
Записи всех выступлений на 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, цель которого автоматизация защиты и верификации для предотвращения различных угроз кибер-безопасности. Основа проекта формализация требований к кибер-безопасности, верификация и защита.
Проект находится на начальной стадии, поэтому в докладах были представлены базовые идеи и текущие направления разработки:
  1. Концепция проекта VeriDevOps.
  2. Обзор литературы по следующим направлениям:
    • извлечение требований безопасности из документов на естественном языке,
    • шаблоны формализации требований,
    • защита и верификация защиты от уязвимостей.
По итогам, приглашаем принять участие к публикации сборника статей - Верификация безопасности - от требований до защиты от уязвимостей.
Дата: пятница 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 г. Рабочая (необработанная) запись на Google Drive.
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 г. Рабочая (необработанная) запись на Google Drive.
Станислав Павлович Кикоть (London Metropolitan University): Магистерские программы по информатике в Великобритании. Дата: среда 2 декабря 2020 г. Рабочая (необработанная) запись на Google Drive.
Дмитрий Александрович Кондратьев (ИСИ СО РАН): Методы и средства для формальной верификации 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 г. Рабочие (необработанные) записи первой части и второй части на Google Drive.
Александр Владимирович Наумчев (Университет Иннополис): Seamless Requirements and specifications. Дата: среда 28 октября 2020 г. Рабочая (необработанная) запись на Google Drive.
Наталья Олеговна Гаранина (ИСИ СО РАН): 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 г. Рабочая (необработанная) запись на Google Drive.