О семинаре

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

  • Извлечение, анализ и моделирование требований
  • Парадигмы моделирования вычислительных систем
  • Методы проектирования систем
  • Архитектуры программных систем
  • Статический и динамический анализ программ
  • Динамическая верификация и мониторинг
  • Автоматизация построения тестов
  • Анализ полноты тестирования
  • Моделирование, измерение и тестирование производительности
  • Анализ защищенности и безопасности вычислительных систем
  • Интеграция различных методов верификации
  • Проблемы внедрения новых технологий в практику разработки
  • Вопросы обучения технологиям разработки и анализа программ

Семинар рассчитан на студентов, аспирантов и их руководителей, а также практиков и специалистов из индустрии. О планах активно принимать участие в семинаре заявили представители компаний Intel, Microsoft, Яндекс и др.

Заседания семинара проходят раз в месяц по четвергам в 17:00, в Институте системного программирования РАН в аудитории 110.

Если вы хотите выступить на семинаре, напишите об этом Петренко Александру Константиновичу.

Ближайшая встреча семинара состоится 16 ноября 2017 года

Будем рады, если вы расскажете коллегам о семинаре и разместите наш постер у вас.

 
Leave a comment

16 ноября: Операционные методы в приложении к слабым моделям памяти

Антон Подкопаев

Антон Подкопаев

Подкопаев Антон Викторович — аспирант кафедры системного программирования математико-механического факультета СПбГУ, сотрудник JetBrains Research (Language Processing Lab).

Антон Подкопаев работает над моделями памяти для языков С/С++ с учетом многопоточности. Модель памяти должна предоставлять гарантии программисту и тем ограничивать пространство возможных поведений программы. С другой стороны, модель памяти обязана учитывать оптимизирующее поведение компиляторов и процессоров, т.к. они влияют на семантику многопоточной программы. Антон Подкопаев предложил операционный вариант модели памяти для языков C/С++ и доказал корректность компиляции для «обещающей’» модели памяти в две модели процессорной архитектуры ARM — ARMv8 POP и ARMv8.3.

Доклад состоится 16 ноября 2017 года в 17:00 в Институте системного программирования РАН имени В.П. Иванникова. Институт располагается в здании по адресу: улица Александра Солженицына, дом 25. Аудитория 110.

Leave a comment

21 сентября: ИНТЕРКОМП-технология создания сложных систем управления

Грудцин Сергей Николаевич

Грудцин Сергей Николаевич

Грудцин Сергей Николаевич — кандидат физико-математических наук, ведущий специалист НПО «Алмаз».

В докладе рассматривается новая отечественная технология ИНТЕРКОМП (ИНТЕРпретация и КОМПиляция) и ее применение для создания новых систем управления.
ИНТЕРКОМП-технология представляет собой по своей сущности, содержанию и реализуемым функциям технологию разработки и создания программного обеспечения с очень компактным кодом, независимым от типа ЭВМ и операционных систем, обеспечивающим высшую степень открытости, масштабируемости, интегрируемости и переносимости.

Доклад состоится 21 сентября 2017 года в 17:00 в Институте системного программирования РАН имени В.П. Иванникова. Институт располагается в здании по адресу: улица Александра Солженицына, дом 25. Аудитория 110.

Leave a comment

27 апреля: Тестирование отказоустойчивости распределенной торговой системы методом эмуляции отказов

Жердер Вадим Меерович

Жердер Вадим Меерович

Костанбаев Сергей Витальевич — кандидат технических наук, главный специалист отдела разработки и сопровождения торгово-клиринговых систем Московской Биржи. Жердер Вадим Меерович — начальник отдела автоматизации тестирования, ПАО Московская биржа.

Костанбаев Сергей Витальевич

Костанбаев Сергей Витальевич

Биржевые торговые системы — высоконагруженные системы, работающие в реальном времени, которые должны удовлетворять высоким требованиям по скорости обработки сообщений и надежности. В докладе описывается архитектура распределенной торговой системы на примере одной из систем Московской биржи и протокол синхронизации состояний узлов (distributed consensus protocol), обеспечивающий ее работу. Специфика требований к торговой системе привела к необходимости разработать новый оригинальный протокол; широко известные протоколы, такие как Raft, оказались неприменимыми. Также будет представлена автоматизированная система тестирования распределенной торговой системы методом эмуляции отказов.

Доклад состоится 27 апреля 2017 года в 17:00 в Институте системного программирования РАН. Институт располагается в здании по адресу: улица Александра Солженицына, дом 25. Аудитория 110.

Leave a comment

16 марта: Доказательство свойств функциональных программ методом насыщения равенствами

Сергей Гречаник

Сергей Гречаник

Гречаник Сергей Александрович — сотрудник Института прикладной математики РАН имени М.В. Келдыша. В 2011 году окончил факультет вычислительной математики и кибернетики МГУ имени М.В. Ломоносова.

В докладе рассматривается метод преобразования программ на нестрогом функциональном языке первого порядка, основанный на комбинации методов насыщения равенствами и суперкомпиляции. Общая идея метода совпадает с идеей насыщения равенствами (предложенного в работе «Equality Saturation: A New Approach to Optimization» Тейта и др. для преобразования императивных программ) и заключается в преобразовании структуры данных, описывающей целое множество программ, а не одну программу. Используемые преобразования, однако, в основном взяты из суперкомпиляции. В рамках метода также предложено преобразование, названное слиянием по бисимуляции, соответствующее доказательству эквивалентности функций по индукции или коиндукции. Показано, что метод применим для индуктивного доказательства эквивалентности программ. Изложение основных идей метода можно найти в препринте «Полипрограммы как представление множеств функциональных программ и преобразования над ними».

Доклад состоится 16 марта 2017 года в 17:00 в Институте системного программирования РАН. Институт располагается в здании по адресу: улица Александра Солженицына, дом 25. Аудитория 110.

Leave a comment

16 февраля: Методы и средства верификации протоколов когерентности памяти

Буренков Владимир Сергеевич

Буренков Владимир Сергеевич

Буренков Владимир Сергеевич — научный сотрудник АО «МЦСТ». В 2012 году окончил факультет «Информатика и системы управления» МГТУ имени Н.Э. Баумана (магистр техники и технологий по направлению «Информатика и вычислительная техника»).

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

Доклад состоится 16 февраля 2017 года в 17:00 в Институте системного программирования РАН. Институт располагается в здании по адресу: улица Александра Солженицына, дом 25. Аудитория 110.

Leave a comment

19 января: Кибербезопасность и бортовые операционные системы

Абрамов Александр Владимирович

Абрамов Александр Владимирович

Абрамов Александр Владимирович — генеральный директор ООО «НТЦ «АМДЭФ». Закончил факультет микроприборов и технической кибернетики МГИЭТ (ТУ). Работал над проектами ГУП НПЦ «Спурт» и НТЦ «АМДЭФ» по созданию аппаратуры помехоустойчивого кодирования сигналов спутниковой связи. Разработчик операционных систем реального времени «Пилот» и «Куб» для встраиваемых систем подвижной радиосвязи.

Фисун Илья Юрьевич

Фисун Илья Юрьевич

Фисун Илья Юрьевич — разработчик в МГТУ имени Н.Э. Баумана. Закончил Московскую финансово-промышленную Академию.

В ходе доклада будет рассмотрен вопрос влияния стандартов и специфики авиационной отрасли на архитектуру операционной системы комплекса бортового оборудования летательного аппарата. Кроме того, будут представлены текущие результаты работы НТЦ «АМДЭФ» над проектом по созданию подсистемы безопасности операционной системы реального времени для гражданской авиации.

Доклад состоится 19 января 2017 года в 17:00 в Институте системного программирования РАН. Институт располагается в здании по адресу: улица Александра Солженицына, дом 25. Аудитория 110.

Leave a comment

17 ноября: Проект Ангара: вычислительные эксперименты на языке программирования F#

Сергей Березин

Сергей Березин

Сергей Березин — к.ф.-м.н., доцент на ВМК МГУ, руководит лабораторией «Информационных технологий в научных исследованиях». Читает авторские курсы лекций «Компьютерная графика» и «Объектно-ориентированное программирование на платформе .NET». В область профессиональных интересов входят научная визуализация, средства хранения и анализа данных, программные средства для проведения сложных вычислительных экспериментов.

Дмитрий Войцеховский

Дмитрий Войцеховский

Дмитрий Войцеховский — закончил ВМК МГУ, прошел стажировку в группе Вычислительных наук Microsoft Research Cambridge, RSDE в лаборатории «Информационных технологий в научных исследованиях». Область профессиональных интересов — современные языки программирования, распределенные и облачные технологии, методы машинного обучения.

Доклад посвящен программному обеспечению для удобного описания и эффективного выполнения вычислительных экспериментов. В докладе будет описан набор компонентов на языке F# под кодовым названием Ангара. Проект Ангара отражает результаты долгосрочного сотрудничества с группой Computational Sciences в Microsoft Research Cambridge. Проект Ангара помогает исследователям строить воспроизводимые вычислительные эксперименты, которые могут выполняться несколько раз с нуля, с одинаковыми результатами. Полная информация о происхождении доступна для каждого результата вычислительного эксперимента, что позволяет точно отследить ход вычислений. Ангара ориентирована на эффективное инкрементальное конструирование вычислительного эксперимента. Новые этапы вычислений могут быть добавлены или изменены с повторным вычислением только результатов, затронутых изменениями. Зачастую это экономит значительное количество времени, так как многие вычислительные эксперименты могут выполняться длительное время и требовать значительных вычислительных ресурсов. Исследователь может наблюдать за промежуточными результатами эксперимента по мере их готовности, тем самым имея возможность оценить ход эксперимента на ранних итерациях, не дожидаясь окончания всего эксперимента.

Проект Ангара доступен на Github.

Доклад состоится 17 ноября в 17:00 в ИСП РАН.

Семинар проходит в Институте системного программирования РАН. Институт располагается в здании по адресу: улица Александра Солженицына, дом 25. Аудитория 110.

Leave a comment

20 октября: Инструментальная поддержка процесса верификации, определенного в документах DO-178B/C

Козырев Владимир Петрович

Козырев Владимир Петрович

Козырев Владимир Петрович — кандидат технических наук, доцент кафедры кибернетики НИЯУ МИФИ, эксперт компании «ДС БАРС».

В докладе рассматривается процесс верификации программ, разрабатываемых в соответствии с требованиями стандартов DO-178B/C, обязательные мероприятия (activities), проводимые в рамках этого процесса, и инструменты, используемые при их проведении. Представляются результаты, полученные в ходе разработки таких инструментов, проводимой в компании «ДС БАРС».

Доклад состоится 20 октября в 17:00 в ИСП РАН.

Наш семинар перемещается в уютное здание Института системного программирования РАН. Он начнется не в 18:00, а в 17:00. Институт располагается в здании по адресу: улица Александра Солженицына, дом 25. Аудитория 110.

2 Comments

15 сентября: Динамическая композиция программных компонентов

Гринкруг Ефим Михайлович — кандидат технических наук, профессор департамента программной инженерии факультета компьютерных наук НИУ ВШЭ. В прошлом — разрабочик ОС М-10 (НИИ Вычислительных комплексов имени М.А. Карцева, эксперт компании Параграф (www.parallelgraphics.com), начальник отдела LuxoftLabs и CТО компании Meshnetics.

Гринкруг Ефим Михайлович

Гринкруг Ефим Михайлович

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

Доклад состоится 15 сентября в 17:00 в ИСП РАН.

Наш семинар перемещается в уютное здание Института системного программирования РАН. В этот раз он начнется не в 18:00, а в 17:00. Институт располагается в здании по адресу: улица Александра Солженицына, дом 25. Аудитория 110. В этот раз прямой трансляции и записи семинара не будет — ждем всех вас лично на семинаре!

Leave a comment

21 апреля: Методы деанонимизации пользователей сети Tor

Сергей Авдошин

Сергей Авдошин

Авдошин Сергей Михайлович — руководитель Департамента программной инженерии НИУ Высшая школа экономики, кандидат технических наук, профессор НИУ ВШЭ.

Александр Лазаренко

Александр Лазаренко

Лазаренко Александр Вячеславович — студент 2 курса бакалавриата образовательной программы «Программная инженерия» НИУ Высшая школа экономики.

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

Послушать доклад можно будет 21 апреля в 18:00 на факультете ВМК МГУ.

Внимание! Важная информация по поводу прохода в МГУ! В связи с усилением пропускной системы, если вы хотите приехать на доклад в МГУ, просим до 12:00 понедельника, 18 апреля, прислать нам на почту sdat@ispras.ru (даже если вы уже были у нас на семинаре до марта этого года) свои ФИО, где и кем работаете, кратко свои достижения (например, ученая степень, звание, если есть). Не забудьте взять с собой паспорт на семинар.

Вы можете присылать свои вопросы как до доклада, так и во время него, по электронной почте sdat@ispras.ru или в твиттер для @sdat_seminar.

Leave a comment