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

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

Ленивый синтез функций по спецификациям первого порядка

February 25

В докладе будет рассказано о недавно предложенном подходе к синтезу нерекурсивных функций по спецификациям, написанным в виде ∀∃-формул первого порядка. Метод основан на ленивом устранении кванторов через последовательное вычисление проекций на основе моделей спецификации и позволяет эффективно синтезировать функции с более чем одним выходом.

Материалы к докладу:

  1. http://www.cs.princeton.edu/~grigoryf/aeval.pdf
  2. http://sat.inesc-id.pt/~mikolas/lpar15.pdf

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