Исследовательская группа

Лаборатория языковых инструментов

Композициональное символьное исполнение императивных программ с кучами

May 21

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

Докладчик: Дмитрий Мордвинов