Г. Ярославцев (АФТУ)
Выполнимость в теориях (Satisfiability modulo theories)

Задача выполнимости в теории (Satisfiability modulo theories, SMT) это задача разрешимости логической формулы, выраженной в классической логике первого порядка с равенством, при наличии дополнительных соотношений, заданных при помощи некоторой теории. Часто использумыми в информатике примерами теорий являются теория вещественных и целых чисел, а также описания поведения различных структур данных, таких как списки, массивы, битовые вектора и т.д.

В докладе будет рассказано о реализации программ, решающих задачу SMT (SMT-солверов) для различных теорий. Доклад основан на курсе лекций Ленордо да Моура, Microsoft Research, прочитанном в рамках летней школы Verification Technologies Systems and Applications 2009
(http://www.mpi-inf.mpg.de/VTSA09/).