Семинар НУЛ ПОИС: Дмитрий Мордвинов "Автоматический вывод реляционных инвариантов для нелинейных систем дизъюнктов Хорна с ограничениями"
На семинаре НУЛ ПОИС выступит Дмитрий Мордвинов (кафедра системного программирования СПбГУ, JetBrains Research).
Индуктивные инварианты являются удобным инструментом доказательства корректности программ. В последнее время стали популярны подходы к автоматическому выводу индуктивных инвариантов как решений систем дизъюнктов Хорна с ограничениями. Однако довольно часто решения нелинейных систем (т.е. систем с правилами, содержащими в посылке более одного применения реляционных символов) оказываются невыразимы с помощью ограничений. В докладе будет введено обобщение понятия индуктивного инварианта для нелинейных систем, которое частично решает эту проблему, а также рассмотрены методы эффективного автоматического вывода таких инвариантов. Будет также рассказано о работе Дмитрия по внедрению механизма вывода реляционных инвариантов в ядро решателя Z3.
Время проведения: 15:10-16:30.