 |
STEP-2024 |
|
|
Российский гибридный семинар STEP-2024
|
| Дмитрий Александрович Кондратьев (ИСИ СО РАН и Новосибирский государственный университет): Соревнование по формальной верификации программ VeHa-2024: два года большого пути | Аннотация: В 2023 году было проведено первое в России соревнование по формальной верификации программ VeHa-2023. Данное соревнование позволило заложить основы для успешного проведения соревнования VeHa-2024 в 2024 году. В данном докладе будут рассмотрены развитие и перспективы серии соревнований VeHa.
После доклада состоится награждение новосибирских дипломантов соревнований VeHa-2024. |
День, дата и время: понедельник 23 декабря 2024 г. 12:40-14:15 в Новосибирске (8:40-10:15 мск). | Семинар пройдет гибридно: в компьютерном классе 305 Главного (Старого) Корпуса Новосибирского Государственного Университета и онлайн в Skype (можно смотреть в браузере). |
| Павел Геннадьевич Емельянов (ИСИ СО РАН и Новосибирский государственный университет): Декомпозиция булевых функций и приложения | Аннотация: Композиционное построение новых объектов - мощный математический инструмент. Обращение композиции - декомпозиция - сложных объектов/систем является важнейшим методологическим приёмом математики. Выявление посредством декомпозиции составляющих систему компонентов позволяет снизить сложность их анализа и преобразований, найти более компактные способы её представления, эксплицировать внутреннюю структуру системы. Понимание сложности задачи декомпозиции систем демонстрирует алгоритмические перспективы работы с ними. Разработка эффективных методов декомпозиции (в том числе, использующих HPC) открывает новые возможности работы со сложными объектами/системами. Одна из самых фундаментальных видов композиции --- декартово произведение. Некоторое обобщение декартова произведения, возникающее в рамках алгебры семейств множеств (Family Algebra), известно как произведение семейств множеств (П.С.М., Family Product). В докладе будут представлены исследования, посвященные обращению (декомпозиции) произведения семейств множеств и некоторые обобщения этой задачи. Задача возникала в разных формулировках в различных областях математики и имеет многочисленные приложения (в некоторых прикладных областях этот вид декомпозиции чрезвычайно важен). Примерами таких областей являются проектирование логических схем, интеллектуальный анализ данных (K&DM) и реляционные БД, теория (гипер)графов, комбинаторная оптимизация, теория игр (simple voting games), структурная теория надежности, онтологическое моделирование и т.д. | День, дата и время: первая часть доклада состоялась в пятница 20 декабря 2024 г., о дне, дате и времени продолжения доклада будет объявлено заблаговременно. | Есть рабочая записи на RuTube-канале ИСИ СО РАН первой первой части доклада (представленной 20декабря 2024г.). О формате продолжения доклада будет объявлено заблаговременно. |
Прошедшие заседания семинара: (в порядке Last-In - First-Out):
| Эридан Доморацкий (Университет ИТМО, Санкт-Петербург): A Relational Solver for Constraint-based Type Inference | Аннотация: We present preliminary results on using relational programming for implementing type inference for a realistic programming language with first-class functions, S-expressions, and pattern-matching. This language, LaMa, has been used for a few years as an educational language to teach compiler construction courses in a number of universities. While not quite being the production-tier programming language, LaMa still is rich enough to, first, demonstrate the majority of relevant techniques in compiler construction domain, and, second, to implement its own compiler.
An important feature of LaMa is the lack of a type system. This brings in all well-known advantages and drawbacks. The motivation for this work was to soften the latter by providing an automatic tool to discover inconsistencies in LaMa programs caused by incoherent usage of data, which is conventionally done by means of a type system. In a nutshell, in our approach a set of constraints is extracted from a program, and the objective is to check if this set of constraints is consistent. While constraint extraction is done in a conventional syntax-directed way and implemented in a functional language, the consistency check is performed relationally. However, as a naïve relational implementation does not perform well, a number of refinements, optimizations and extensions to the vanilla miniKanren needs to be applied. In the talk we give an overview of LaMa programming language, devised type system, relational type inference approach, and describe various refinement of vanilla relational solver. (Совместная работа с Д.Ю. Булычевым, см. статью на arXiv.) |
Дата: пятница 10 декабря 2024 г. | Рабочая (необработанная) запись на RuTube-канале ИСИ СО РАН. ( Есть презентация доклада.) |
| Николай Аркадьевич Прокопьев (Казанский (Приволжский) федеральный университет): Прагматически-ориентированные модели и методы обработки естественно-языковых вопросно-ответных текстов | Аннотация: В докладе представлены модели и методы, направленные на обработку естественно-языковых ответов обучающихся в ситуации контроля знаний. Изложены следующие результаты исследования и разработки:
|
Дата: пятница 29 ноября 2024 г. | Рабочая (необработанная) запись на RuTube-канале ИСИ СО РАН. ( Есть презентация доклада.) |
| Мария Наумчева (Университет Тулузы): UOOR: an Object-Oriented Approach for Requirements engineering | Аннотация: In industrial practice, requirements are an indispensable element of any serious software project. In the academic study of software engineering, requirements are one of the heavily researched subjects. And yet requirements as practiced in industry makes shockingly sparse use of the concepts propounded in the requirements literature. The talk starts from an assumption about the causes for this situation, and proposes a remedy to redress it. The posited explanation is that change is the major factor affecting the practical application of even the best-intentioned requirements techniques. Requirement methods that assume that requirements can be set once and for all to guide the development are doomed. The proposed remedy is a requirements method, called UOOR, which unifies many known requirements concepts and a few new ones in a framework entirely devised to accommodate and support seamless change throughout the project lifecycle. The UOOR method (the acronym stands for Unified Object-Oriented Requirements) encompasses the commonly used requirements techniques, namely, scenarios, and integrates them into the seamless software development process. We introduce the notion of seamless requirements traceability, which relies on propagation of traceability links, themselves based on formal properties of relations between project artifacts. As a proof of concept we present a Traceability tool, to be integrated into a general-purpose IDE, that provides the ability to link requirements to other software project artifacts, to display notifications of change in requirements and to trace those changes to the related project elements. | Дата: пятница 15 ноября 2024 г. | Рабочая (необработанная) запись на RuTube-канале ИСИ СО РАН. |
| PSSV-2024: Семинар по семантике, спецификации и верификации программ: теория и приложения | Международный семинар по семантике, спецификации и верификации программ (PSSV) имеет 15-летнюю историю. Он был запущен в 2010 году, чтобы стать площадкой для сотрудничества между исследователями в области семантики, спецификации и проверки программ из Содружества Независимых Государств и международных коллег.
C историей и тематикой PSSV можно познакомиться на странице семинара 2023 г..
Программа семинара PSSV-2024 включала 5 приглашенных, 4 регулярных и 4 коротких доклада. Одновременно с семинаром PSSV-2024 прошли вторые российские соревнования по верификации программ Verification Hackathon VeHa-2024. |
Даты: суббота 19 и воскресенье 20 октября 2024 г. | Записи выступлений, презентации докладов и предварительные публикации доступны по ссылкам в Программе семинара. |
| Андрей Михайлович Миронов (Московский государственный университет им. М.В. Ломоносова): Процессный подход к верификации криптографических протоколов | Аннотация: В докладе изложена новая математическая модель криптографических протоколов, и приводятся примеры применения этой модели для решения задач верификации криптографических протоколов. Криптографические протоколы -- это коммуникационные протоколы, реализованные с применением криптографических алгоритмов для решения задач защиты информации, в рамках которого стороны информационного взаимодействия последовательно выполняют определенные действия и обмениваются сообщениями. Они используются, например, в электронных платежах, электронных процедурах голосования, системах доступа к конфиденциальным данным, и т.д. Ошибки в криптографических протоколах могут привести к большому ущербу, поэтому необходимо использовать математические методы для обоснования различных свойств корректности и безопасности криптографических протоколов. В докладе изложен новый метод формальной верификации криптографических протоколов. Для моделирования криптографических протоколов в докладе вводятся понятия последовательного и распределенного процессов. Предлагаемый подход предназначен для построения формальных доказательств корректности для заведомо корректных криптографических протоколов. Особенностью модели протоколов является её простота по сравнению с другими моделями протоколов, основанных на логических формулах или на алгебраических процессных выражениях. Участники протоколов представляются в виде графов, представляющих системы переходов. Действия, выполняемые участниками, являются метками этих переходов. Методы обоснования корректности протоколов, рассматриваемые в настоящей статье, связаны с рассуждениями для графов, которые более просты и наглядны по сравнению с методами, основанными на построении логического вывода в логических и алгебраических моделях протоколов. |
Дата: пятница 11 октября 2024 г. | Есть презентация доклада. |
| Антонина Николаевна Непейвода (Московский государственный технический университет им. Н. Э. Баумана): Обзор выразительных возможностей формальных языков с захватом в память | Аннотация: В докладе рассмотрены два класса языков, привлекшие значительный интерес исследователей в XXI веке: языки расширенных регулярных выражений и языки уравнений в словах. Будет приведён обзор существующих результатов о выразительных возможностях данных классов языков, а также обсуждение их взаимосвязи. | Дата: пятница 27 сентября 2024 г. | Рабочая (необработанная) запись на RuTube-канале ИСИ СО РАН. ( Есть презентация доклада.) |
| Евгений Сергеевич Муравьев (Университет Иннополис): Краткий обзор дистрибутивов Linux | Аннотация: В канун День Рождения Linux (одного из четырех) был дан краткий обзор истории и архитектуры (а также личные впечатления) дистрибутивов Linux, с которыми есть опыт работы. | Дата: пятница 13 сентября 2024 г. | Рабочая (необработанная) запись на YouTube-канале и на RuTube-канале ИСИ СО РАН. ( Есть презентация доклада.) |
| Сергей Михайлович Старолетов(Алтайский государственный технический университет): Классификация коммитов в git репозиториях для поиска наиболее частых исправлений ошибок в системном программном обеспечении (ядро Linux и проекты кибефизических систем) | Аннотация: В средах системного программного обеспечения циркулирует огромное количество информации, поэтому крайне важно использовать эту информацию для улучшения их работы. Одной из таких систем является ядро Linux, которое не только поставляется с полностью открытым исходным кодом, но и предоставляет исчерпывающую историю о разработке в своем git-репозитории. Вычисляя расстояния между сообщениями об исправлении ошибок, превращая их в вектора и группируя в кластеры, мы далее можем эффективно классифицировать и выявлять наиболее часто возникающие ошибки. Наш подход применяется к нескольким важным частям ядра Linux, что позволяет понять, что происходит с ошибками в различных его подсистемах. В результате мы показываем сводку исправлений ошибок в таких частях ядра Linux, как kernel, sched, mm, net, irq, x86 и Arm64. Киберфизические системы представляют собой симбиоз многоуровневых систем управления и учитывают физические аспекты функционирования целевых объектов. Ошибки в таких системах могут быть связаны как с неправильной организацией кода и работой аппаратных средств, так и с неверным пониманием физических законов и их численной аппроксимацией. Продолжая предыдущую работу, мы применяем технологии автоматизированного анализа коммитов в git-репозиториях некоторых известных киберфизических систем с последующей классификацией собранных сообщений о фиксации изменений, написанных разработчиками таких систем. В работе мы обсуждаем выявленные сильные ключевые слова и обобщенные сообщения об исправлениях, которые способны показать основные классы ошибок в этих проектах. Публикации по теме:
|
Дата: среда 21 августа 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.) |
| Алексей Недоря: Архитектурное программирование. Языки Арс и Арвиль | Аннотация: Архитектурное программирование (АРП) - это технология, обеспечивающая корректность описания архитектуры программной системы в течении всего времени жизни системы. Описание архитектуры состоит из описания устройства системы, описание частей (компонент) и их взаимодействия. В АРП описание архитектуры делается с помощью формальной нотации и является входным данным для компиляторов и/или систем сборки. Для практической проверки жизнеспособности технологии разрабатываются два экспериментальных языка: Арс - описание системы и Арвиль - разработка компонент. | Дата: среда 3 июля 2024 г. | Есть рабочие записи на YouTube-канале ИСИ СО РАН первой и второй частей доклада. ( Есть презентация доклада.) |
| Артем Сергеевич Бурмяков (Университет Иннополис): Towards a Tractable Exact Test for Global Multiprocessor Fixed Priority Scheduling | Аннотация: An exact schedulability analysis of a system of sporadic tasks to be executed upon a multiprocessor platform is proved to be a weakly NP-hard computational problem. The available exact tests suffer from a high computation time and memory requirement, which make them intractable for large realistic real-time systems. On the other hand, the available approximate sufficient tests, which are faster and consume less memory, are very pessimistic in provisioning the execution requirements of a given system. Motivated by these observations, we propose an exact schedulability test for constrained-deadline sporadic tasks under global multiprocessor fixed-priority scheduler (GFP), which is significantly faster and consumes less memory, compared to any other available exact test. To derive a faster test, we exploit the idea of a state-space pruning, aiming at reducing the number of feasible system states to be examined by the test. The resulted test is multiple orders of magnitude faster with respect to other state-of-the-art exact tests. The C++ implementation of our test is publicly available. | Даты: первая часть - среда 6 марта, вторая часть - среда 22 мая, заключительная третья часть - среда 26 июня 2024 г. | Есть рабочие записи на YouTube-канале ИСИ СО РАН первой, второй и третьей частей доклада, а также презентация доклада. ( Есть презентация доклада.) |
| Николай Вячеславович Шилов (Университет Иннополис): "Теория всего": унификация паттернов дизайна алгоритмов (метода отката, ветвей и границ, жадных алгоритмов, метода разделяй и властвуй, и динамического программирования...) | Аннотация: Курс проектирования и анализа алгоритмов является обязательной составляющей учебных программ по информатике всех уровней. В университетах этот курс обязательно включает изучение структур данных, методы проектирования алгоритмов, теорию сложности и т.д. Этот курс знакомит с такими методами проектирования алгоритмов, как жадные алгоритмы, динамическое программирование, метод разделяй и властвуй, метод отката, метод ветвей и границ. Обычно знакомство с этими методами происходит на примерах. Но они могут быть (полу)формализованы в виде рекурсивных "паттернов" (с использованием map и reduce), специфицированы условиями частичной и/или тотальной корректности и обоснованы (доказаны) методом Флойда верификации алгоритмов. | Даты: первая часть - среда 22 мая, вторая (заключительная) часть - среда 19 июня 2024 г. | Рабочие (необработанные) записи на YouTube-канале ИСИ СО РАН первой и второй частей доклада. ( Есть презентация доклада.) |
| Александр Иванович Легалов (Высшая школа экономики, Москва): Процедурно-параметрический полиморфизм и его интеграция с языком программирования C | Аннотация: Разработка больших программ часто связана с инкрементальным расширением уже написанного кода. При этом встречаются ситуации, когда альтернативные программные объекты формируются во время выполнения. В этом случае для их идентификации и последующей обработки используется либо явная проверка типа, либо один из методов динамического полиморфизма, предоставляемый тем или иным языком программирования. Расширение программы за счет новых альтернатив, добавляемых в ходе разработки, может привести к модификации уже написанного кода. В этих случаях для минимизации изменений вместо явной проверки типов обычно применяются методы динамического полиморфизма. Из них к широко известным можно отнести ОО полиморфизм, использование интерфейсов в Go и типажей в Rust. Процедурно-параметрический полиморфизм является альтернативным подходом. Рассматриваются его особенности и интеграция с языком программирования C. Представлены дополнительные синтаксические конструкции, ориентированные на поддержку подхода, их возможности и варианты реализации. Приводятся примеры эволюционного расширения кода для простых ситуаций демонстрирующие большую гибкость по сравнению с существующими подходами. Также рассматривается моделирование паттернов проектирования, повышение надежности за счет обертки над ненадежными языковыми конструкциями языка C. | Дата: среда 29 мая 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.) |
| По сложившейся традиции нашего семинара участники семинара приглашаются присоединиться к заседаниям Spring/Summer Young Researchers' Colloquium on Software Engineering (SYRCoSE). | SYRCoSE
организуется ежегодно начиная с 2007 широко известными специалистами в программной инженерии и программировании Александром Константиновичем Петренко (Институт системного программирования РАН, Москва) и Андреем Николаевичем Тереховым (Санкт-Петербургский Государственный Университет).
Программа Коллоквиума SYRCoSE-2023 включала два пригашенных (пленарных) доклада:
|
Даты: среда 29 мая - четверг 30 мая 2024 г. | Презентации приглашенных докладов будут доступны позже. |
| Евгений Александрович Зуев (Университет Иннополис): Modelling C++ inheritance and dynamic semantics using a C++ virtual machine | Аннотация: Доклад представляет экспериментальный программный стенд, предназначенный для моделирования ключевых свойств языка С++, включая механизмы наследования (единичного, множественного и виртуального) и полиморфизма. Стенд включает компилятор представительного подмножества языка С++ в низкоуровневый интерпретируемый язык IML и виртуальную машину, реализующую аспекты динамической семантики С++ в части полиморфизма (виртуальные функции с перекрытиями, динамическое приведение типов) и распределения динамической памяти. Стенд может использоваться как инструмент моделирования различных программных конфигураций для оценки эффективности применения моделируемых свойств С++. Проект выполняется группой студентов университета Иннополис под руководством автора доклада. | Дата: среда 8 мая 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. ( Есть презентация доклада.) |
| Ершовская лекция 2024 г. | 19 апреля - День Рождения Андрея Петровича Ершова. По сложившейся традиции мы приглашаем участников семинара присоединиться к
традиционной Ершовской лекции, организуемой Институтом систем информатики им. А.П. Ершова.
В 2024 г. лекцию прочитал член Правления ключевых ИТ-ассоциаций России – АПКИТ и Руссофт Владимир Васильевич Рубанов, тема лекции Риски и преимущества открытости исходных кодов вашего программного обеспечения. Аннотация: В докладе рассмотрен феномен открытого исходного кода (open-source) программных проектов. Будет представлен анализ основных движущих сил и типов участников открытых проектов. Приведены примеры важных проектов и участия различных компаний в их разработке. Центральное место доклада занимает анализ преимуществ и рисков, которые возникают в связи с открытием исходного кода того или иного продукта или компонента. Показано наличие оптимальной точки открытия кода (в плане момента времени и объема открытия) в зависимости от ситуации. Отклонение от такой точки для конкретного проекта приводит либо к "недооткрытию" (under-open-sourcing), либо к "переоткрытию" (over-open-sourcing), что непосредственно влияет на развитие продукта. Наконец, в докладе будет рассмотрена история участия в проектах с открытым кодом компании Huawei, которая из состояния отрицания необходимости открытия кода за считаные годы превратилась в одного из мировых лидеров open-source движения. |
Дата: четверг 18 апреля 2024 г. | Есть запись лекции на YouTube-канале ИСИ СО РАН. |
| Андрей Валентинович Климов (Институт прикладной математики им. М.В. Келдыша РАН, Москва): Научное наследие В.Ф. Турчина и его кибернетические основания математики | Аннотация: Научно-философское наследие Валентина Федоровича Турчина (14.02.1931–07.04.2010) состоит из трех частей:
(1) философской, объясняющей его эволюционную концепцию с центральным понятием метасистемного перехода как кванта эволюции, — книга "Феномен науки: Кибернетический подход к эволюции" [1977 (англ.), 1993, 2003 (рус.)]; (2) социальной: обсуждение эволюции общества и человека — книга "Инерция страха: Социализм и тоталитаризм" [1977]; (3) научной: суперкомпиляция в программировании и кибернетические основания математики — статья "A constructive interpretation of the full set theory" [1987] и отчеты "The Cybernetic Foundation of Mathematics" [1983]. В докладе кратко охарактеризованы первые части, суперкомпиляция опущена и дано введение в кибернетические основания математики — потенциалистской интерпретации, являющейся расширением алгоритмического конструктивизма А.А. Маркова и Э. Бишопа путем введения (модели) математика в теорию — таким образом, что удалась конструктивная интерпретация теории множеств ZF. |
Дата: среда 10 апреля 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Александр Валентинович Когтенков: Объектно-ориентированное программирование без встроенных типов | Аннотация: Насколько оправдано упрощение объектно-ориентированного языка программирования при доказательстве каких-то его свойств? Что можно написать на ОО языке без встроенных типов, арифметических операторов, операторов сравнения, условных инструкций и инструкций цикла? Теоретически возможность объявлять классы, переменные и процедуры, а также создавать и присваивать объекты, обращаться к переменным и вызывать процедуры должно хватить, чтобы реализовать любую программу. Но как это выглядит на практике? На семинаре будет разобран код простого примера, отвечающего на этот вопрос.
Несмотря на фундаментальную природу, работа не носит научного характера, доступна широкому кругу специалистов профильных специальностей, может быть интересна разработчикам и исследователям языков программирования и трансляторов. |
Дата: среда 3 апреля 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Алексей Юрьевич Зубарев (Институт систем информатики СО РАН, Новосибирск): Взаимосвязи семантик и эквивалентностей непрерывно-временных сетей Петри со слабой временной стратегией | Аннотация: Непрерывно-временные сети Петри — это расширение сетей Петри, в которых каждому переходу ставятся в соответствие временной интервал его срабатывания и локальные часы. Данная модель позволяет учитывать как функциональные (качественные), так и реально-временные (количественные) свойства моделируемых систем. Рассматриваются непрерывно-временные сети Петри со слабой временной стратегией, где ход модельного времени не форсирует срабатывания сетевых переходов. Для данной модели и ее модификаций разрабатываются и исследуются семантические представления и поведенческие эквивалентности в дихотомиях «интерливинг-частичный порядок» и «линейное-ветвящееся время». Кроме того, в контексте «слабых» непрерывно-временных сетей Петри предлагается метод редукции пространства состояний за счёт их дискретизации. | Дата: среда 20 марта 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Маргарита Владимировна Коровина (Институт систем информатики СО РАН, Новосибирск): Automated Reasoning with Continuous Data | Семинар STEP-2024 продолжает традицию специальных заседаний в Международный женский день: ru-STEP-2021, ru-STEP-2022 и STEP-2023.
Аннотация доклада In this talk we report on ongoing research on solving non-linear constraints over the reals occurring in a wide range of applications, starting with program verification, ranging over verification of real-world designs all the way to automation of formally verified proofs of mathematical statements. In our framework methods from Computable Analysis and Automated Reasoning are combined to meet efficiency and expressiveness. This approach is applicable to a large number of constraints involving computable non-linear functions, piecewise polynomial splines, transcendental functions and solutions of polynomial differential equations. We give an introduction to the ksmt calculus for checking satisfiability of non-linear constraints in a CDCL style way inspired by advances in SAT solving. Along proof search ksmt resolves two types of conflicts: linear and non-linear. Linear conflicts are delegated to a decision procedure for linear real arithmetic and non-linear conflicts are resolved by local linearisations separating the solution set and the current conflict. We show that the ksmt calculus is a σ-complete decision procedure for bounded problems. |
Дата: среда 28 февраля 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. |
| Всеслав Станиславович Секорин (Тверской государственный университет): Выразительные возможности операторов частичной неподвижной точки для конечных и бесконечных систем | Аннотация: В работе рассмотрены различные семантики частичной фиксированной точки для конечных и бесконечных алгебраических систем. В частности, показано, что операторы частичной фиксированной точки рассматриваемых семантик можно промоделировать оператором инфляционной фиксированной точки в тех алгебраических системах, в которых есть строгий частичный порядок со сколь угодно длинными цепями. Также, например, показано что элиминировать оператор частичной фиксированной точки можно только в тех теориях, в которых любой такой оператор зацикливается за конечное число шагов. Доклад представляет материалы и результаты кандидатской диссертации на соискание ученой степени кандидата физико-математических наук по специальности 1.1.5. "Математическая логика, алгебра, теория чисел и дискретная математика". | Дата: среда 28 февраля 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Игорь Сергеевич Ануреев (Институт систем информатики СО РАН, Новосибирск): Логика распознавания последовательностей состояний SSRL (State Sequences Recognition Logic) и примеры её применения для формализации темпоральных требований к управляющим программ | Аннотация: Предлагается формализм для описания свойств последовательностей состояний, порождаемых системой переходов (state transition system). Этот формализм под рабочим названием SSRL (State Sequences Recognition Logic) позволяет задавать свойства поведения системы переходов, определяемого как множество последовательностей состояний, порождаемых отношением перехода. В отличие от LTL, он поддерживает императивные вставки, позволяющие сохранять информацию в именованных компонентах состояний (аналог let в функциональных языках программирования), называемых атрибутами. В тоже время он имеет более простую систему модальностей и более жесткий порядок их комбинирования по сравнению с LTL. Даются методология и примеры его применения для формализации темпоральных требований к управляющим программ, на которые он, в первую очередь, ориентирован. Цель разработки формализма применительно к решению этой задачи - расширить область применимости ранее представленного на семинаре формализма EDTL (Event-Driven Temporal Logic), который позиционируется как язык описания темпоральных требований, ориентированный на инженеров. В качестве обоснования большей выразительной силы нового формализма рассматриваются примеры требований, невыразимых на EDTL, а также определяется формальная семантика EDTL на SSRL. | Дата: среда 14 февраля 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Алексей Недоря: О "граблях" в инициализации объектов в современных языках программирования | Аннотация: Рассмотрены инициализации объектов в современных языках программирования Swift/Kotlin/Тривиль. (Выступление в рамках темы "филология программирования", поднятой А.В. Коноваловым во время "Дня Проблем 2023", про язык Тривиль см. выступления Алексей Недори "Опыт разработки и реализации языка Тривиль" и "Интенсивное программирование: язык Тривиль" на семинаре STEP-2023.) | Дата: пятница 2 февраля 2024 г. | Рабочая (необработанная) запись на YouTube-канале ИСИ СО РАН. (Есть презентация доклада.) |
| Заседание семинара посвященное Всемирному Дню Логики (https://en.wikipedia.org/wiki/World_Logic_Day) |
В 2024 г. мы продолжили традицию семинара (см. Logic Day 2023, Logic Day 2022 и
Logic Day 2021)
совместных заседаний с
Математическим Клубом Университета Иннополис (см. Telegram-беседу Logic Day in Innopolis ).
А так как Всемирный День Логики установлен UNESCO (United Nations Educational, Scientific and Cultural Organization), то у нас были сообщения по спектру тем Education, Science, Culture…
|
Обычно мы выбираем дату так, что бы не конкурировать с другими событиями в честь Всемирного Дня Логики. Наш встреча состоялась вечером в пятницу 26 января и утром в субботу 27 января. | Ссылки на презентацию доклада В. Крйновича и на записи выступлений И.О. Пыльцына и Л. Меркина даны в колонке слева. |