Добрый день всем!

Во *вторник 13 октября* 2020 в *13 часов* приглашаем на *онлайн*-семинар в
Zoom, чтобы послушать предзащитный доклад:

   -

   *Дмитрий Александрович Мордвинов* (СПбГУ)

*Дизъюнкты Хорна с ограничениями в контексте формальной верификации
   программ *(по материалам кандидатской диссертации)

Аннотация

С ростом популярности SMT-решателей появилось большое количество подходов и
инструментов автоматической верификации программного обеспечения,
написанного на самых разных языках программирования. При всём разнообразии
этих подходов, языков и парадигм программирования становится важным
сведение задачи формальной верификации программы к единому представлению. В
докладе будет рассмотрено одно из таких представлений: дизъюнкты Хорна с
ограничениями (Constrained Horn Clauses).

В первой части доклада мы вспомним историю области и введем необходимые
определения. Мы увидим, что по любой императивной программе можно
автоматически построить систему дизъюнктов Хорна с ограничениями, такую,
что её решения в точности соответствуют всем индуктивным инвариантам
исходной программы. В случае функциональных программ такие решения будут
соответствовать уточняющим типам (refinement types) программы. Будет
рассказано о существующих инструментах автоматического решения систем
дизъюнктов Хорна с ограничениями и о применении этих инструментов для
анализа байткода Java и LLVM.

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

Файлы автореферата и диссертации доступны:

   -

   автореферат
   https://drive.google.com/file/d/1jZJOxwqaOQa8cx23ZEMboRXA8pAxNFrQ
   -

   диссертация
   h
   <https://www.iis.nsk.su/files/Dissertaciya_Mordvinova_ot_15.09.2020.pdf>
   ttps://www.iis.nsk.su/files/Dissertaciya_Mordvinova_ot_15.09.2020.pdf
   <https://www.iis.nsk.su/files/Dissertaciya_Mordvinova_ot_15.09.2020.pdf>
   на сайте дисс-совета
   h <https://www.iis.nsk.su/institute/dissert/preliminary_procedure>
   ttps://www.iis.nsk.su/institute/dissert/preliminary_procedure
   <https://www.iis.nsk.su/institute/dissert/preliminary_procedure>

Информация о Zoom-сеансе:

Topic: Дмитрий Мордвинов - Дизъюнкты Хорна с ограничениями в контексте
формальной верификации программ
Time: Oct 13, 2020 13:00 Moscow

Join Zoom Meeting
https://us02web.zoom.us/j/82206910430?pwd=Qm05ek1BOGh4SkswUFpOV2FXVVIxUT09

Meeting ID: 822 0691 0430
Passcode: 350248

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

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

До встречи в Сети!

Андрей Климов

Ответить