13 июня - семинар в ИСП РАН
12 views
Skip to first unread message
Eugene Kornykhin
May 24, 2019, 11:56:26 AM5/24/19
to Семинар <<Технологии разработки и анализа программ>>
Доброго времени суток!
13 июня состоится заседание городского научно-практического семинара
"Технологии разработки и анализа программ" в ИСП РАН. О своей работе
расскажет аспирант кафедры системного программирования СПбГУ,
сотрудник JetBrains Research Дмитрий Мордвинов. Его научные интересы
лежат в области доказательства правильности программ. Доклад
называется "Реляционные инварианты как решения нелинейных систем
дизъюнктов Хорна с ограничениями".
Индуктивные инварианты являются удобным инструментом доказательства
корректности программ. В последнее время популярны подходы к
автоматическому выводу индуктивных инвариантов как решений систем
дизъюнктов Хорна с ограничениями. Однако довольно часто решения
нелинейных систем (т.е. систем с правилами, содержащими в посылке
более одного применения реляционных символов) невыразимы в языке
ограничений. В докладе будет введено обобщение понятия индуктивного
инварианта для нелинейных систем, которое частично решает эту
проблему, а также рассмотрены методы эффективного автоматического
вывода таких инвариантов. В частности, будет рассказано о работе
докладчика по внедрению механизма вывода реляционных инвариантов в
ядро решателя Z3.
Мероприятие пройдет в ИСП РАН по адресу г. Москва, ул.
Александра Солженицына, дом 25. Четверг, 13 июня, начало в 17:00.
Будем рады, если Вы расскажете о докладе потенциальным
заинтересованным коллегам, не получающим рассылку, к письму приложен
постер семинара.
С уважением,
Евгений Корныхин,
семинар "Технологии разработки и анализа программ" (руководитель -
Петренко Александр Константинович)
http://sdat.ispras.ru
13 июня состоится заседание городского научно-практического семинара
"Технологии разработки и анализа программ" в ИСП РАН. О своей работе
расскажет аспирант кафедры системного программирования СПбГУ,
сотрудник JetBrains Research Дмитрий Мордвинов. Его научные интересы
лежат в области доказательства правильности программ. Доклад
называется "Реляционные инварианты как решения нелинейных систем
дизъюнктов Хорна с ограничениями".
Индуктивные инварианты являются удобным инструментом доказательства
корректности программ. В последнее время популярны подходы к
автоматическому выводу индуктивных инвариантов как решений систем
дизъюнктов Хорна с ограничениями. Однако довольно часто решения
нелинейных систем (т.е. систем с правилами, содержащими в посылке
более одного применения реляционных символов) невыразимы в языке
ограничений. В докладе будет введено обобщение понятия индуктивного
инварианта для нелинейных систем, которое частично решает эту
проблему, а также рассмотрены методы эффективного автоматического
вывода таких инвариантов. В частности, будет рассказано о работе
докладчика по внедрению механизма вывода реляционных инвариантов в
ядро решателя Z3.
Мероприятие пройдет в ИСП РАН по адресу г. Москва, ул.
Александра Солженицына, дом 25. Четверг, 13 июня, начало в 17:00.
Будем рады, если Вы расскажете о докладе потенциальным
заинтересованным коллегам, не получающим рассылку, к письму приложен
постер семинара.
С уважением,
Евгений Корныхин,
семинар "Технологии разработки и анализа программ" (руководитель -
Петренко Александр Константинович)
http://sdat.ispras.ru
Eugene Kornykhin
Jun 11, 2019, 5:36:50 AM6/11/19
to Семинар <<Технологии разработки и анализа программ>>
Добрый летний день! В этот четверг, 13 июня, в 17:00 состоится семинар
"Технологии разработки и анализа программ" в ИСП РАН. Дмитрий
Мордвинов из JetBrains Research расскажет о реляционных инвариантах
как решениях нелинейных систем дизъюнктов Хорна с ограничениями.
Подробности - ниже в письме и на сайте семинара http://sdat.ispras.ru.
С уважением,
Евгений Корныхин
"Технологии разработки и анализа программ" в ИСП РАН. Дмитрий
Мордвинов из JetBrains Research расскажет о реляционных инвариантах
как решениях нелинейных систем дизъюнктов Хорна с ограничениями.
Подробности - ниже в письме и на сайте семинара http://sdat.ispras.ru.
С уважением,
Евгений Корныхин
Reply all
Reply to author
Forward
0 new messages