13 июня: Реляционные инварианты как решения нелинейных систем дизъюнктов Хорна с ограничениями

Дмитрий Мордвинов

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

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

Доклад состоится 13 июня 2019 года в 17:00 в Институте системного программирования РАН имени В.П.Иванникова. Адрес института: улица Александра Солженицына, дом 25. Аудитория 110.