JetBrains Research — наука, меняющая мир

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

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

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

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

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

25.02.2019, 17:15.

Место: ауд. 3248, мат-мех. факультет СПбГУ, Старый Петергоф, Университетский пр-т, д. 28