Шишкин Евгений Сергеевич

Шишкин Евгений Сергеевич — ведущий исследователь, научный отдел компании ИнфоТеКС. Научные интересы: формальная верификация моделей реагирующих систем, методы формальной спецификации, SAT/SMT решатели и их применение в задачах верификации программ.

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

Роль доверенного посредника в контексте блокчейнов выполняют
специальные программы — смарт-контракты.

Смарт-контракты определяют бизнес-логику взаимодействия множества
участников и управляют их ценными активами: криптовалютой, токенами,
правами на объекты и т.д.

Ошибки в смарт-контрактах приводили ранее к многомиллионным потерям,
при этом количество относительно громких инцидентов растет с каждым
месяцем.

Доклад посвящен задаче повышения надёжности смарт-контрактов
при помощи символьной верификации моделей программ, в первую
очередь интерес представляют программы на языке Solidity.

Затрагиваются такие темы:

1. Актуальность решаемой задачи с научной и экономической точек зрения;
2. Новейшие подходы к формальной верификации смарт-контрактов
   вообще, и, символьной верификации моделей в частности;
3. Элементы технологии верификации смарт-контрактов, используемой авторами доклада
   в практических проектах по верификации смарт-контрактов;
4. Научно-техническая новизна некоторых подходов, используемых авторами доклада.

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

Слайды доклада для скачивания.

Запись Zoom-конференции:

Владимир Шелехов

Шелехов Владимир Иванович — к.т.н. зав.лаб. Системного Программирования, Институт Систем Информатики им. А.П. Ершова СО РАН, Новосибирск.

Аннотация (орфография и пунктуация авторские): Одной из предпосылок исследований стало осознание безнадежности императивного программирования. В целях построения адекватной технологии программирования рассматривается классы программ: программы-функции, программы-процессы, языковые процессоры и другие.

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

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

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

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

Дмитрий Мордвинов

Дмитрий Мордвинов — аспирант кафедры системного программирования СПбГУ, сотрудник JetBrains Research.

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

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

Кознов Дмитрий Владимирович

Кознов Дмитрий Владимирович — доктор технических наук, профессор кафедры системного программирования СПбГУ.

В компаниях по разработке ПО и в отдельных программных проектах к настоящему времени накапливается большое количество данных – требования, ошибки и отчёты об ошибках, запросы на изменения, комментарии к коду и документация, исходные тексты программ и их версии, тесты и т.д. Важной характеристикой этих данных является возрастающий объем и наличие разнообразной текстовой информации. При этом остро стоит вопрос автоматического управления этими данными, в частности, управление дублированием. В докладе будет рассказано о задаче управления дублированными отчётами об ошибках (crash reports) на примере индустриального решения компании JetBrains, а также о задаче поиска и рефакторинга нечётких дубликатов в JavaDoc-документации. Будут также рассмотрены различные индустриальные постановки задачи управления нечёткими дубликатами как в программном коде, так и в других software-данных.

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

Самонов Александр Валерьянович

Самонов Александр Валерьянович — старший научный сотрудник Военно-космической академии имени А.Ф. Можайского, кандидат технических наук, доцент.

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

- графово-текстовая метамодель формализованного представления комплекса требований и описаний архитектуры в виде набора взаимосвязанных fUML-диаграмм;

- методика реализации программно-управляемого процесса разработки и верификации при помощи разработанных моделей и алгоритмов.

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

Вячеслав Любченко

Любченко Вячеслав Селиверстович — независимый разработчик. Научные интересы: автоматное программирование.

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

Здесь можно скачать слайды доклада в формате PDF.

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

Шишкин Евгений Сергеевич

Шишкин Евгений Сергеевич — ведущий исследователь, научный отдел компании ИнфоТеКС. Научные интересы: дедуктивные методы формальной верификации, методы формальной спецификации, построение специализированных доменных логик, спецификация и верификация распределенных и реагирующих систем, функциональное программирование.

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

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

В основном докладе планируется затронуть такие темы:

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

Помимо доклада планируется провести дискуссию со специалистами ИСП РАН и, возможно, приглашенными экспертами по программированию и аудиту смарт-контрактов для выработки общего взгляда на проблему и пути решения.

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

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

Непейвода Антонина Николаевна

Непейвода Антонина Николаевна — м.н.с. центра мультипроцессорных систем ИПС им. А.К. Айламазяна РАН. Научные интересы: преобразование и анализ программ, формальные языки и грамматики.

В докладе будет рассмотрена проблема преобразования и верификации программ, манипулирующих строками. Предложен новый метод описания свойств параметризованных конфигураций анализируемой программы посредством языка уравнений в словах. Уравнение в словах есть выражение вида w = u, где w, u - слова в алфавите, являющимся объединением алфавита символов и алфавита строковых переменных. За счет использования языка уравнений в словах можно выявить и кратко выразить некоторые нетривиальные свойства допустимых значений параметров.

Метод развивается в терминах суперкомпиляции - метода преобразования программ, основанного на развертке и свертке дерева параметризованных состояний оптимизируемой программы. На базе идеи описания свойств строковых параметров посредством уравнений в словах построен модельный суперкомпилятор MSCP-A - оптимизатор программ на языке программирования Рефал.

Расширенный вариант аннотации доклада можно прочитать по этой ссылке.

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

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

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

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

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

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

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

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

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