Семинар по метавычислениям во вторник 13 октября 2020 в 13:00 в Zoom'е

[Andrei Klimov andrei_AT_klimov . net]

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

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

   -

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

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

Аннотация

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

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

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

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

   -

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

   диссертация
   h
   
   ttps://www.iis.nsk.su/files/Dissertaciya_Mordvinova_ot_15.09.2020.pdf
   
   на сайте дисс-совета
   h 
   ttps://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’а есть приятная возможность
установить фон, если вы не хотите показывать окружение, в котором
находитесь.

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

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

RE: Поздравляем Андрея Петровича Немытых с юбилеем!

[Александр Коновалов a . v . konovalov87_AT_mail . ru]

Дорогой Андрей Петрович!

Я присоединяюсь к поздравлениям Вашего коллеги. Хочу пожелать счастья, 
здоровья, творческих успехов и условий для творческих успехов! Ведь «служенье 
муз не терпит суеты».

 

Всего самого лучшего!
Александр Коновалов

 

From: Andrei Klimov andrei_AT_klimov.net  
Sent: Friday, October 9, 2020 5:39 PM
To: refal@botik.ru
Subject: Поздравляем Андрея Петровича Немытых с юбилеем!

 

Дорогой Андрей Петрович,

 

От имени всего рефал-сообщества позвольте поздравить Вас со знаменательной 
датой, которая символизирует Вашу зрелость, мудрость и большую историю успехов!

 

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

 

С уважением,

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