Семинар НУЛ ПОИС: Дмитрий Мордвинов "Автоматический вывод реляционных инвариантов для нелинейных систем дизъюнктов Хорна с ограничениями"

На семинаре НУЛ ПОИС выступит Дмитрий Мордвинов  (кафедра системного программирования СПбГУ, JetBrains Research).

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

Время проведения: 15:10-16:30.