Исследовательская группа
Лаборатория языковых инструментов
Интерполяция Крейга
December 17
Доклад будет посвящен понятию интерполяции Крейга в логике первого порядка. Будет затронуто приложение интарполяции к формальной верификации программ; в частности, будет рассказано об использовании интерполянтов для вывода индуктивных инвариантов и резюмированию функций. Также будет кратко рассказано про методы построения интерполянтов.
Докладчик: Михаил Костицын