Computer Science Summer in Russia (CSSR)

Прошло почти полвека с того времени, когда Роберт Флойд опубликовал первую работу о том, как придать программам математически-корректную («формальную») семантику. Минуло двадцать лет с тех пор, как Давид Шмидт опубликовал статью "О необходимости популярной формальной семантики". За эти годы было разработано множество индивидуальных формальных семантик, но (как отмечал Д. Шмидт) научных экспертов по формальной семантике пока значительно больше, чем инженеров-программистов, которые ее используют. В то же время мы видим значительную активность в исследованиях по формальной семантике и ее приложениях.

Этот курс для тех, кто хочет понять, что такое «формальная семантика языков программирования». Поэтому он начинается со знакомством с типами формальной семантики на примере эзотерического языка программирования, продолжается построением формальных семантик для игрушечного (но уже не эзотерического) языка программирования, а заканчивается знакомством с современными вопросами, например – формальной семантикой указателей (в терминах исчисления алиасов Бертрана Мейера).

В этом курсе Вы сможете:

• узнать зачем нужна формальная семантика программ

• понять принципы операционной, денотационной и аксиоматической семантики

• познакомиться с операционной, денотационной и аксиоматической семантикой игрушечного языка программирования

• почувствовать, где возникают трудности при формализации семантики реальных языков программирования

• познакомиться с примером проблемно-ориентированной формальной семантики (для указателей)

• узнать об использовании разных формальных семантик в верификации программ

• обсудить место формальной семантики программ в реальной программной инженерии, в том числе в разработке ПО для космических аппаратов

Кандидат физико-математических наук, доцент АНО ВО «Университет Иннополис». Специалист в области теории программирования и прикладной логики.

Работал в Sydney University of Technology (Австралия), Nazarbayev University (Казахстан), University of Canterbury, Christchurch (Новая Зеландия), Korea Advanced Institute of Science and Technology, Chung-Ang University и Samsung Advanced Technology Training Institute (Южная Корея).

В настоящее время исследовательские интересы связаны с математическими основаниями формальных методов и их приложениями для анализа программных, информационных, распределенных и мультиагентных систем. Текущая работа связана с исследованиями по проекту «Платформенно-независимый подход к формальной спецификации и верификации стандартных математических функций».

Цель этого курса - познакомить слушателей с теорией языков программирования - одним из активно разрабатываемых разделов информатики. Мы начнём с элементарного введения в основные идеи, понятия, факты и инструменты теории, после чего разберем примеры актуальных исследований, связанных с языком программирования Haskell, результаты которых регулярно освещаются на важнейших конференциях в этой области: POPL (Principles of Programming Languages, Принципы языков программирования) и ICFP (International Conference on Functional Programming, Международная конференция по функциональному программированию).

Темы второй части курса будут излагаться в виде обзора, из которого слушатели получат базовое представление о применяемых методах исследований в теории языков программирования. Всем слушателям будет предоставлен подробный электронный конспект лекций и список литературы для более глубокого изучения.

Старший преподаватель кафедры информатики и вычислительного эксперимента Института математики, механики и компьютерных наук имени И.И. Воровича Южного федерального университета (Ростов-на-Дону), разработчик в JetBrains. Преподает лекции по функциональному программированию, теории вычислений и теории языков программирования.

Член комитета по стандартизации языка Haskell и член наблюдательного комитета компилятора GHC языка Haskell.

Перевёл на русский язык и редактировал переводы нескольких книг по языку Haskell и теории языков программирования. Автор книги "Haskell in Depth" (доступна в рамках программы раннего доступа издательства Manning Publications).

В этом курсе Вы познакомитесь с некоторыми современными промышленными и академическими инструментами тестирования и формальной верификации. Курс охватывает следующие методы в сфере тестирования:

• разработка через тестирование (TDD),
• разработка на основе поведенческой спецификации (BDD),
• автоматическое создание модульных тестов с помощью MS Spec Explorer,
• подход MS Code Contracts,

а также следующие методы верификации:

• верификация методом проверки моделей с помощью Spin в среде iSpin;
• написание контрактов для C-программ с помощью метода слабейшего предусловия (Weakest Precondition),
• верификация кибер-физических систем и обзор примеров в системе автоматического доказательства KeYmaera.

Доцент АлтГТУ им. Ползунова, кандидат физико-математических наук, специалист в области моделирования и тестирования распределенных программных систем на основе автоматных мультиагентных моделей.

Имеет богатый опыт работы в программной индустрии. Автор книги "Основы тестирования и верификации программного обеспечения", изд-во Лань, 2018 г.

Проверка моделей — это метод для автоматической верификации соответствия модели системы и ее формальной спецификации. Он используется для проверки корректности программного обеспечения, оборудования и других параллельных и распределенных систем в отношении таких свойств, как свобода от блокировок, выполнение инвариантов и ответов на запросы и т. п. В методе проверки моделей обычно сравнивается конечная модель системы с ее спецификацией, выраженной в каком-либо формализме. Зачастую в качестве такого формализма выступает темпоральная логика.

В этом курсе мы рассмотрим базовые логики и алгоритмы проверки моделей, а также варианты метода для вероятностных моделей и моделей реального времени. Метод будет иллюстрироваться различными примерами. Будет предоставлен обзор программных инструментов проверки моделей, включая SPIN и PRISM.

Старший научный сотрудник Института систем информатики им. А.П. Ершова, специалист в области логики и ее приложений для верификации мультиагентных систем, распределенных алгоритмов.

Работала в Университете Чун ан, Сеул, Южная Корея, участвовала в проекте Computal Европейского Союза по вычислимому анализу. Преподает курсы по формальным методам программной инженерии, в том числе методам верификации, в Новосибирском Государственном Университете.

В этом курсе мы представим введение в концептуально простой, но в тоже время мощный и эффективный метод верификации систем с бесконечным числом состояний и параметризованных систем. Метод использует моделирование понятия достижимости между состояниями системы посредством выводимости (доказуемости) в классической логике первого порядка.

При таком моделировании чтобы продемонстрировать безопасное поведение системы, т.е. недостижимость опасных состояний, достаточно показать, что конкретная формула логики первого порядка не выводима. В описываемом методе решение задачи невыводимости поручается автоматической процедуре поиска контрмодели.

Мы изложим теоретические основания метода и обсудим многочисленные применения к задачам верификации, относящимся к

• системам с ненадежными каналами связи,
• протоколам для поддержки когерентности кэшей,
• параметризованным массивам конечных автоматов,
• слабым моделям памяти,
• системам переписывания термов и задачам из популярной математики.

Далее мы покажем относительную полноту метода по отношению к любому другому методу, использующему регулярные инварианты. То есть, при достаточно общих предположениях, если безопасность системы/протокола может быть показана при помощи регулярных инвариантов, то она может быть показана и FCM-методом. Мы заметим, что с практической точки зрения FCМ-метод почти всегда оказывается быстрее известных альтернатив.

Руководитель исследовательской группы по верификации департамента компьютерных наук университета г. Ливерпуль. Его исследования относятся к трем взаимосвязанным областям: методы автоматической верификации (в особенности для параметризованных систем и систем с бесконечным числом состояний); методы машинных рассуждений с приложениями к верификации и математике; методы компьютерной безопасности.

Автор более 100 научных работ. Алексей Лисица является председателем-учредителем и членом руководящего комитета серии семинаров VPT (Verification and Program Transformation), шесть выпусков которых проводились eжегодно в ассоциации с ключевыми конференциями CAV или ETAPS.

Алексей был приглашенным экспертом в проекте SC ^ 2, Horizon 2020 по проверке выполнимости (SAT solving) и символьным вычислениям. В настоящее время является руководителем совместного научно-индустриального проекта KTP (Партнерство по передаче знаний) по безопасной обработке данных и технологиям, основанным на блокчейне.

Во многих прикладных областях до сих пор отмечается нехватка логических средств верификации программного обеспечения. Например, разработка программ управления с использованием приложения Matlab-Simulink(R) использует симуляцию как основной метод тестирования. Но до сих пор нет общепринятых методов, которые могли бы гарантировать корректное поведение систем автоматического управления во всех состояниях.


С другой стороны, в последние 20 лет мы наблюдаем существенный прогресс в разработке специализированных формализмов, в том числе модальных логик, связанных с прикладными предметными областями. Методы машинного доказательства становятся все более эффективными и доступными даже для нестандартных логических формализмов. Однако решение задачи формализации предметной области в рамках той или иной логики по-прежнему остается ключевым этапом, который не допускает автоматизации и должен быть сделан «вручную».


В этом курсе Вы познакомитесь со средствами, которые призваны облегчить данный этап, и основаны на предметно-ориентированных языках (Domain-specific Languages, DSLs). DSLs представляют собой формализмы, достаточно выразительные для описания входов в широко распространенных форматах, используемыми инженерными средствами, такими как, например, Matlab-Simulink(R). Кроме того, их гибкость позволяет формулировать доказательства в рамках различных логических формализмов.


Данный курс основан на примере из области автоматического управления. Для начала мы попробуем описать корректную систему автоматического управления с помощью средства Matlab-Simulink(R), а затем перейдем к уточнению при помощи предметно-ориентированных языков. В качестве средства верификации системы управления будет использоваться системой автоматического доказательства KeYmaera.

Томас Баар - выпускник Берлинского университета им. Гумбольдта, получил степень PhD в университете Карлсруэ (ныне Технологический институт Карлсруэ), Германия. С 2011 работает в должности профессора по специализации в инженерии ПО и баз данных в Университете прикладных технических и экономических наук, г. Берлин.

В сферу научных интересов Томаса входят методы машинных рассуждений, конструирование языков программирования и моделирования, в том числе предметно-ориентированных языков для верификации гибридных систем.

Хайде Брандтштедтер - выпускница Берлинского технического университета, получила степень PhD в Мюнхенском техническом университете. В 2008 присоединилась к лаборатории Сименс в Берлине, где занималась роторной динамикой крупноразмерных электрических агрегатов и торсионным анализом трансмиссии. С апреля 2018 г. работает в должности профессора в Университете прикладных технических и экономических наук, г. Берлин.

Научные интересы связаны с математическим моделированием динамических систем и теорией управления, в частности, управлением в скользящем режиме.

Построение компиляторов — одна из самых старых и зрелых областей информатики. Несмотря на долгую историю, начавшуюся в 1950-е годы, эта область постоянно изменяется и развивается. Классические учебники устаревают и не справляются с вопросом подготовки студентов и практикующих специалистов к решению научно-исследовательских и промышленных задач.

Данный краткий курс углублённого изучения компиляторов дополняет традиционные бакалаврские или магистерские лекции по компиляции и эволюции программного обеспечения примерами задач в области компиляции языков четвёртого поколения и предметно-ориентированных языков, модернизации устаревших систем, обратной разработки и т. п. Лекции данного курса основаны на опыте преподавания в ведущих европейских вузах, научном руководстве магистрантами и работе в компании Raincode Labs - крупнейшем в мире независимом производителе промышленных компиляторов.

В курсе мы рассмотрим множество примеров из современных программных пакетов и свежих академических статей, а также из ежедневной практики промышленных проектов языковой разработки, поддержки и миграции.

На первой лекции мы поищем примеры окружающих нас программных языков и компиляторов, сместив акцент с традиционного системного программного обеспечения на предметно-ориентированные пакеты и «языковые верстаки». Также мы кратко обсудим конкретные инструменты, облегчающие жизнь несистемным программистам, желающим просто автоматизировать рутинные и хрупкие задачи обработки конфигурационных файлов или манипуляции данных в XML, JSON и подобных форматах.

Вторая лекция будет технической, мы углубимся в изучение конкретных техник и подходов, появившихся или развившихся за последнее десятилетие: извлечения, сходимости и адаптирования грамматик, двунаправленных преобразований, тестирования, внедрения и т. д.

На последней лекции будут рассмотрены несколько недостаточно проработанных вопросов, которые будут интересны студентам и аспирантам, ищущим тему для исследований.

Заместитель директора по науке в бельгийской компании Raincode Labs, занимающейся предоставлением услуг по разработке и поддержке компиляторов, а также консультациями по связанными с этим вопросам.

Защитил кандидатскую диссертацию в Свободном университете Амстердама по направлению языковой инжинерии и грамматических технологий. Над этой темой он также работал в немецком Университете Кобленца-Ландау, нидерландском Центре математики и информатики и в Университете Амстердама, где также был активно вовлечён в учебный процесс, осуществлял научное руководство, поддерживал и расширял связи университета с индустрией.

Интересы и научная активность сосредоточены вокруг таких тем, как оценка качества программного обеспечения, анализ и трансформации программного кода, моделирование, метамоделирование и мегамоделирование, парадигмы программирования, декларативное и функциональное программирование, поддержка и обновление устаревших систем.

Во время лекции мы расскажем вам о самом интересном и актуальном, а именно:


- О компании Uma.Tech;

- Раскроем тему продуктовой разработки и того, как Data Science помогает в создании новых продуктов;

- Рассмотрим популярную методологию CRISP-DM;

- Решим реальную задачу прогнозирования оттока пользователей на основе предложенной схемы процесса;

- Предложим к выполнению "домашнее задание".

Руководитель Отдела анализа данных компании Uma.Tech. Станислав занимается анализом данных и внедрением методов машинного обучения более 3,5 лет. На данный момент управляет группой специалистов в компании Uma.Tech, которая внедряет модели машинного обучения, разрабатывает рекомендательные системы и занимается вопросами Computer Vision.

Практически каждая предметная область характерна богатыми системами терминов, которые используются специалистами в формальном и неформальном виде для документирования полученных знаний. В этой связи возникает и необходимость документирования терминов. Так, например, были развиты классификации в биологии и химии, своды специализированных терминологических систем в виде глоссариев, тезаурусов, таксономий и онтологий, представляющие определения терминов и взаимосвязей между ними.


Как правило, специализированные технические тексты, например, документация или спецификация технических узлов и агрегатов, опирается на богатую терминологию, которая включается в документацию в виде глоссария. Некоторые своды терминов являются стандартами на государственном или высшем профессиональном уровне, например, Общероссийский Классификатор Видов Экономической Деятельности, Международная Классификация Болезней и многие другие.


Формализованные терминологии применяются в информационных системах для решения задач аннотирования, поиска, интеграции информации, анализа текстов на естественном языке. На сегодняшний день в сети Интернет доступны сотни математически формализованных терминологических систем, которые используются для решения информационных задач, в естественнонаучных и технических предметных областях.


В этом курсе Вы узнаете о технологии работы с терминологическими системами на основе методов формальной логики. Вы узнаете про аппарат дескрипционных логик, которые применяются в течение более двадцати лет как математическая основа для формализации и анализа терминологических систем, онтологий. В частности, на дескрипционных логиках базируются известные компьютерные языки-стандарты, применяемые для публикации онтологий в Интернет. В курсе будет рассказано о том, как применять средства логики при разработке онтологий и как использовать методы машинных рассуждений для анализа, структурирования и выявления дефектов в онтологиях.

Старший научный сотрудник Института Систем Информатики им. А.П. Ершова и старший преподаватель Новосибиирского государственного университета. Работал в качестве приглашенного профессора и старшего научного сотрудника на факультете информатики Университета Райерсона, Торонто, и в Институте Искусственного Интеллекта при Университете г. Ульм, Германия.

Рецензент журнала ACM «Transactions on Computational Logic» и член программных комитетов ведущих конференций по тематике Искусственного Интеллекта, включая AAAI и IJCAI, а также международного воркшопа по дескрипционным логикам и других конференций близкой тематики.

Основные научные интересы: методы представления знаний, машинных рассуждений и доказательств, инженерия онтологий, методы рассуждения о действиях.

Специалист в области логики и ее приложений в инженерии данных и знаний.

После окончания мехмата МГУ защитил диссертацию по теории соответствия в модальной логике. Затем после стажировки в Яндексе работал в должности научного сотрудника в Лондонском университете над фундаментальными проблемами доступа к данным на основе онтологий.

В настоящее время - научный сотрудник департамента компьютерных наук Оксфордского университета в группе теории баз данных.

Старший преподаватель кафедр общей информатики и систем информатики Новосибирского государственного университета. Читает лекции по дискретной математике, математической логике и теории языков программирования.

Автор языка и программной реализации Russell - системы, предназначенной для представления формальных дедуктивных систем и машинных рассуждений в них.

Руководитель исследовательской группы по верификации департамента компьютерных наук университета г. Ливерпуль. Его исследования относятся к трем взаимосвязанным областям: методы автоматической верификации (в особенности для параметризованных систем и систем с бесконечным числом состояний); методы машинных рассуждений с приложениями к верификации и математике; методы компьютерной безопасности.

Автор более 100 научных работ. Алексей Лисица является председателем-учредителем и членом руководящего комитета серии семинаров VPT (Verification and Program Transformation), шесть выпусков которых проводились eжегодно в ассоциации с ключевыми конференциями CAV или ETAPS.

Алексей был приглашенным экспертом в проекте SC ^ 2, Horizon 2020 по проверке выполнимости (SAT solving) и символьным вычислениям. В настоящее время является руководителем совместного научно-индустриального проекта KTP (Партнерство по передаче знаний) по безопасной обработке данных и технологиям, основанным на блокчейне.

Специалист в области высоконагруженных распределенных систем и глубокого обучения. Преподает курсы по данным направлениям в Новосибирском Государственном Университете и является представителем NVIDIA Deep Learning Institute в НГУ.

Имеет богатый опыт работы в промышленных проектах с использованием данных технологий. Примером одного их проектов является система умного паркинга http://green-pay.ru

Специалист в области анализа данных и адаптивного управления. Работает в Институте систем информатики им. А.П. Ершова в тесном сотрудничестве с Лабораторией теории вычислимости и прикладной логики Института математики С.Л. Соболева.


Имеет практический опыт разработки систем извлечения знаний и прогнозирования в различных областях, включая медицину, финансы и биоинформатику. Занимается исследованиями в области создания интеллектуальных самообучающихся робототехнических систем.