Доброго времени суток!
13 июня состоится заседание городского научно-практического семинара
"Технологии разработки и анализа программ" в ИСП РАН. О своей работе
расскажет аспирант кафедры системного программирования СПбГУ,
сотрудник JetBrains Research Дмитрий Мордвинов. Его научные интересы
лежат в области доказательства правильности программ. Доклад
называется "Реляционные инварианты как решения нелинейных систем
дизъюнктов Хорна с ограничениями".
Индуктивные инварианты являются удобным инструментом доказательства
корректности программ. В последнее время популярны подходы к
автоматическому выводу индуктивных инвариантов как решений систем
дизъюнктов Хорна с ограничениями. Однако довольно часто решения
нелинейных систем (т.е. систем с правилами, содержащими в посылке
более одного применения реляционных символов) невыразимы в языке
ограничений. В докладе будет введено обобщение понятия индуктивного
инварианта для нелинейных систем, которое частично решает эту
проблему, а также рассмотрены методы эффективного автоматического
вывода таких инвариантов. В частности, будет рассказано о работе
докладчика по внедрению механизма вывода реляционных инвариантов в
ядро решателя Z3.
Мероприятие пройдет в ИСП РАН по адресу г. Москва, ул.
Александра Солженицына, дом 25. Четверг, 13 июня, начало в 17:00.
Будем рады, если Вы расскажете о докладе потенциальным
заинтересованным коллегам, не получающим рассылку, к письму приложен
постер семинара.
С уважением,
Евгений Корныхин,
семинар "Технологии разработки и анализа программ" (руководитель -
Петренко Александр Константинович)
http://sdat.ispras.ru