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

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

Докладчик: Михаил Костицын