Добрый день всем! Во *вторник 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’а есть приятная возможность установить фон, если вы не хотите показывать окружение, в котором находитесь. До встречи в Сети! Андрей Климов
