Седьмая конференция по программной инженерии и организации информации
23 апреля 2022 года
Online
Участник SEIM-2019
Презентация доклада на SEIM-2019 Бейджи участников SEIM-2019

Конференция SEIM-2019

Форум для молодых ученых

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

Подробнее о конференции
Бесплатное участие
Публикация в CEUR

ISSN 1613-0073

Индексация в РИНЦ
Награда за лучшую статью
Поддержка иногородним участникам

Тематика конференции

включает следующие темы, но не ограничивается ими:
  • Алгоритмы и структуры данных
  • Большие данные
  • Верификация
  • Визуальные языки
  • Виртуализация
  • Высокопроизводительные вычисления
  • E-commerce / e-government
  • Интеллектуальный анализ данных
  • Интернет вещей
  • Информационная безопасность
  • Компиляторы
  • Краудсорсинг
  • Машинное обучение
  • Методы информационного поиска
  • Мобильные системы
  • Моделирование
  • (Не)реляционные базы данных
  • Облачные системы
  • Обработка естественных языков
  • Операционные системы и системы реального времени
  • Программно-конфигурируемые сети
  • Распределенные системы
  • Рекомендательные системы и персонализация
  • Робототехника
  • Семантическая паутина
  • Сети и телекоммуникации
  • Социальные сети
  • Статический и динамический анализ программ
  • Теоретические основы информатики
  • Теория кодирования
  • Тестирование
  • Управление разработкой ПО
  • Хранение данных
  • Цифровая обработка сигналов
  • Эмпирическая программная инженерия
  • Языки программирования
Ilya Sergey

Keynote Speaker

Ilya Sergey

Ilya is an Associate Professor at the School of Computing of National University of Singapore, where he leads the Verified Systems Engineering lab. He also holds a joint appointment at Yale-NUS College and is a lead language designer at Zilliqa, a Singapore FinTech start-up.

Ilya received his MSc from St Petersburg University and PhD from KU Leuven. Before joining NUS, he was a postdoctoral researcher at IMDEA Software Institute and a faculty at University College London. Prior to starting his academic career, he worked as a software developer at JetBrains.

Ilya does research in programming language design and implementation, software verification, distributed systems, program synthesis and repair. He is a recipient of distinguished paper awards at POPL and PLDI, the 2019 Dahl-Nygaard Junior Prize, the 2021 Yale-NUS Distinguished Researcher Award, and a Google Faculty Research Award.


Title

Deductive Synthesis of Heap-Manipulating Programs: Sound, Expressive, Fast


Abstract:

In my talk, I will describe a deductive approach for synthesising imperative programs with pointers from declarative specifications expressed in Separation Logic. The approach treats logical program specifications, given in the form or pre- and postconditions with a pure and a spatial part, as proof goals, and provides an algorithm for rule-directed program construction based on the shape of the symbolic heap footprint a desired program manipulates. The program synthesis algorithm rests on the novel framework of Synthetic Separation Logic (SSL). The produced executable programs are correct by construction, in the sense that they satisfy the ascribed specifications, and are accompanied by complete proof derivations (i.e., certificates), which can be checked independently by a third-party verifier.

The approach has been implemented as a proof search engine for SSL in a form a program synthesiser. For efficiency, the engine exploits properties of SSL specifications, aggressively relying on a version of the Frame Rule and commutativity of separating conjunction to prune the search space. I will explain and showcase the use of SSL on characteristic examples, describe the design of out tool, and report on the experience of using it to synthesise a series of benchmark programs manipulating with heap-based linked data structures. I will also tell about some recent advances of automatically certifying synthesised programs in the Coq proof assistant.

Важные даты

Принять участие

Со статьей

К участию принимаются оригинальные статьи на русском и английском языках. Работу необходимо подать до 20 февраля.

В качестве слушателя

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

Место проведения

В связи с эпидемиологической обстановкой конференция пройдет в онлайн-формате

Офис JetBrains

Кантемировская ул. 2, Санкт-Петербург, Россия

По всем вопросам: