Заседания 2017/2018 учебного года
Смирнов Денис
Идентификация исполняемых файлов с помощью битовых распределений
В докладе будет рассказано о проведенном исследовании внутренней структуры исполняемых файлов разных форматов на битовом уровне. Цель исследования: решение задачи об эффективном способе нанесения цифрового водяного знака на программное обеспечение.
Будет небольшое вступление о том, какие виды водяных знаков применяются на данный момент, какие проблемы они решают и какие трудности возникают при их использовании, а затем описание подхода по внедрению водяного знака определенного типа с помощью распределений битов внутри файла. Также будет кратко рассказано о МАКе - многоуровневой архитектуре кода, наборе инструментов, созданном и активно развивающемся на нашей кафедре, и дающем возможность компилировать необычные исполняемый файлы с очень высокой степенью обфускации.
Соломенников Дмитрий Игнатьевич
Компилятор Flow и его оптимизация
Доклад посвящен языку программирования Flow, разработанному компанией
Area9 Innovation, компилятору этого языка, а также оптимизации
компилятора в процессе разработки.
Язык Flow разрабатывается
компанией Area9 Innovation с 2010 года и представляет собой
кросс-платформенный язык программирования, предназначенный для создания
сложных графических интерфейсов. Продукты, созданные с помощью этого
языка, использует более 12 миллионов человек по всему миру. В магазинах
App Store и Google Play представлено несколько мобильных приложений,
также разработанных с помощью Flow.
В докладе будут даны описание
языка, описание внутренней структуры компилятора, а также описание
исполнительной машины и библиотеки времени выполнения языка.
Рассматриваются следующие вопросы:
- общая структура компилятора;
- структура лексического и синтаксического анализатора;
- исполнительная машина Flow;
- генераторы кода под разные платформы.
Также
в докладе будут представлены методы, применявшиеся при оптимизации
компилятора и исполнительной машины, описаны ряд использованных
высокоуровневых и низкоуровневых способов оптимизации.
Материалы к докладу:
Аннотация и план доклада
Брыксин Тимофей Александрович
Автоматическое выявление возможных рефакторингов в коде при помощи ансамблей кластеризаторов
В докладе будет рассказано об исследованиях в области автоматического выявления рефакторингов объектно-ориентированного кода и о плагине ArchitectureReloaded к IntelliJ IDEA, основанном на методах кластеризации. Цель плагина – анализировать код открытого в IDEA проекта и предлагать программисту возможные направления для рефакторинга, улучшающие такие характеристики, как сопряжение (cohesion), связаность (coupling) и ряд других метрик объектно-ориентированных проектов. Также в докладе будет кратко рассказано о ряде других проектов, выполняемых в рамках нашей исследовательской группы на стыке программной инженерии и машинного обучения.
Материалы к докладу:
Презентация
Литвинов Юрий Викторович
Глубокое метамоделирование
В докладе будет кратко рассказано о текущих научных тенденциях в области визуальных языков и более подробно – про формализацию их синтаксиса, в частности, про один популярный сейчас подход: "глубокое метамоделирование". Данный подход рассматривает визуальный язык как иерархию моделей, каждая из которых является экземпляром предыдущей, при этом элемент каждой модели может рассматриваться одновременно и как объект, и как класс (то есть как тип объектов модели более низкого уровня), свойства которого могут распространяться на сразу несколько уровней иерархии. Оказывается, что такой подход может помочь значительно упростить определения существующих языков (например, UML), а также весьма перспективен для использования в предметно-ориентированном моделировании. Будет также рассказано про опыт реализации этого подхода в системе REAL.NET [1].
Материалы к докладу:
1. Среда предметно-ориентированного визуального моделирования REAL.NET
/ Литвинов Ю.В., Кузьмина Е.В., Небогатиков И.Ю. [и др.] //
СПИСОК-2017. Материалы 7-й всероссийской научной конференции по
проблемам информатики. 2017. С. 80–89.
Волкова Марина Владимировна
Рандомизированные алгоритмы оценивания параметров инкубационных процессов в
условиях неопределенностей и конечного числа наблюдений
В настоящее время методы измерения и прогнозирования динамической прочности материалов сложны и не стандартизированы. Рассматривается способ обработки экспериментальных данных, основанный на критерии инкубационного времени. Обычно на практике имеется лишь небольшое число измерений со случайными ошибками и ограниченной статистической информацией, поскольку динамические эксперименты являются трудоемкими и на проведение каждого отдельного испытания требуется много времени. Это сильно ограничивает количество доступных методов обработки данных, если только мы не удовлетворены приблизительными эвристическими решениями. В предположении о симметричности шума используется метод знако-возмущенных сумм для определения конечных доверительных интервалов с заданной доверительной вероятностью. Показано, что нескольких экспериментальных точек достаточно, чтобы определить значение прочностного параметра с точностью, подходящей для инженерных расчетов. Работоспособность предложенного метода продемонстрирована на примере обработки ряда экспериментов по динамическому разрушению горных пород.
Ерофеева Виктория Александровна
Адаптивное управление группами робототехнических устройств на основе
мультиагентных технологий
Рассматривается задача отслеживания траекторий группы движущихся объектов с помощью набора распределенных в пространстве сенсоров. Нахождение оптимального значения параметров достигается с определенным уровнем качества за счет использования мультиагентного алгоритма. В работе предлагается два подхода к отслеживанию траекторий: на основе циклической стохастической аппроксимации и линейных матричных неравенств. Для распределения заданий в группе устройств рассматривается циклический подход с ограничениями.
Кижаева Наталья Александровна
Исследование паттернов в текстах на основе динамических моделей
Полина Соколова
Обзор современных цифровых платформ «умного» дома
«Умный» дом — это система автоматизации жилых помещений, которая
включает в себя контроль и управление отоплением, освещением,
вентиляцией, кондиционированием и безопасностью. Кроме того, составной
частью умного дома является «умная» бытовая техника. Рынок «умных» домов
— это новая технологическая ниша, которая только начинает
формироваться. В докладе будут рассмотрены перспективы развития этого
рынка, основные стандарты и технологии Интернета вещей, а также
существующие платформы «умного» дома.
Рене Хаберланд (ЛЭТИ)
Логический язык
программирования как язык спецификации и верификации для динамической памяти
Цель семинара рассмотреть подход к решению проблемы верификации программ с динамической памятью с помощью логического языка программирования, который использован в качестве языка спецификации и верификации. Рассматриваются следующие вопросы:
- анализ существующих ограничений выразимости и выявление причин расходимости между языками спецификации и верификации;
- критерии реализации алгоритмов верификации динамической памяти на основе логического языка программирования (на базе абстрактной машины Уоррена);
- автоматизация
верификации куч, как синтаксического перебора абстрактных предикатов,
основаного на пошаговой обработке граней графа кучи.
Баклановский М.В., Кривошеин Б.Н., Сибиряков А.Е., Ханов А.Р.
Асимметричный маркерный процессинг
В докладе будет показан путь от простой на первый взгляд идеи переноса части вычислений в ПЛИС до универсальной технологии организации вычислений в гетерогенной мультипроцессорной системе. Более подробно будет рассказано:
- о построении и формальной верификации протокола транспортного уровня, ответственного за передачу управления от одного процессора к другому;
- об измерении времени, которое тратится на передачу управления с использованием различных областей общей памяти на платформе Zybo Zync-7000.
Кроме этого будет повторён доклад о данной технологической разработке, сделанный на международном форуме Мироэлектроника 2017, на котором наша разработка по защите ПО от ревёрс-инжиниринга стала победителем в номинации Кибербезопасность.
Амелин Константин Сергеевич
Гражданские БПЛА: современные технологии и направления, проблемы и их возможные решения
В связи с увеличением роста применения сверхлегких БПЛА при решении
задач гражданского применения, к таким аппаратам возрастают требования в
техническом плане, к применяемому программному и математическому
обеспечению, к системам безопасности, а также растет необходимость в
унификации БПЛА и увеличения их потенциала. На семинаре будут
представлены актуальные задачи при разработке сверхлегких БПЛА для
гражданского применения, методы их решения, проблемы реализации таких
решений, а также актуальные текущие проблемы при решении новых задач.
Такие проблемы возникают при создании новых систем автопилотирования
БПЛА, обработки данных, оптимизации полета БПЛА, при работе с
дополнительными исполнительными механизмами. Будут представлены новые
актуальные направления развития гражданских БПЛА, проблемы безопасности,
а также задачи применения лазерных технологий при работе как
обособленных БПЛА, так и их групп.
Мордвинов Дмитрий Александрович
О неограниченной верификации, решателях дизъюнктов Хорна и символьном исполнении
За последние 3 года появилось несколько верификаторов, эффективно доказывающих корректность программ с рекурсией неограниченной глубины [1, 2, 3], работающих во многих ситуациях на порядок лучше аналогов. Общая их черта состоит в том, что они сводят задачу верификации кода к задаче автоматического доказательства теорем над системой дизъюнктов Хорна.
В докладе планируется кратко рассмотреть общие принципы работы таких верификаторов (пути к кодированию программ в систему дизъюнктов Хорна, алгоритмы поиска индуктивного инварианта и контрпримеров), а также некоторые продвижения докладчика в этой области (алгоритмы синхронизации дизъюнктов Хорна [4], адаптация символьного исполнения императивных программ для случая неограниченной рекурсии).
Литвинов Юрий Викторович
Обзор школы LASER-2017
Школа LASER-2017 (https://www.laser-foundation.org/)
проходила с 9 по 17 сентября на о. Эльба, темой школы этого года стало
программное обеспечение в робототехнике. Школа проходила в формате коротких
лекционных курсов (как правило, из 6 лекций), читавшихся видными представителями
сообщества, приглашённого доклада Андрея Николаевича и небольшого количества
студенческих презентаций. Лекции читали:
* Davide Brugali, University of Bergamo --- о линейках программных
продуктов, feature-oriented анализе и его применении в робототехнике;
* Rodolphe Gelin, Softbank Robotics --- о человекоподобных роботах;
* Ashish Kapoor, Microsoft Research --- о безопасном управлении
квадрокоптерами, вероятностных темпоральных логиках и симуляции;
* Nenad Medvidovic, University of Southern California --- об архитектуре ПО
вообще и робототехнических систем в частности;
* Bertrand Meyer, Politecnico di Milano --- о параллелизме и применении
Eiffel в робототехнике;
* Issa Nesnas, NASA Jet Propulsion Laboratory --- о робототехнике в
космических исследованиях вообще и архитектуре бортового ПО роверов в
частности;
* Hiroshi “Gitchang” Okuno, Waseda University and Kyoto University --- о
распознавании звука, локализации источников звука, разделении и анализе звуковых
потоков, роли восприятия звука в человекомашинном взаимодействии.
Ханов Артур Рафаэльеаич
Безопасность смарт-контрактов в криптовалюте Ethereum
Ethereum - одна из наиболее быстроразвивающихся криптовалют. Она позволяет не только обмениваться денежными средствами. В ее основе лежат так называемые смарт-контракты. Это программы на особом языке, которые выполняются всей децентрализованной сетью и могут содержать достаточно сложную логику. Важнейшим аспектом развития Ethereum является ее безопасность. Поэтому программы-смарт-контракты необходимо уметь проверять на предмет того, насколько описанные в них условия устойчивы к атакам злоумышленника. Так год назад произошла история, в которой из-за уязвимого смарт-контракта злоумышленник чуть не украл более 50 миллионов долларов. Возможно ли ограничить логику работы контрактов таким образом, чтобы они были по-прежнему достаточно выразительны для написания и в то же время верифицируемы? Ответ на этот вопрос и предстоит получить участникам семинара.
Стипендия А.Н. Терехова
