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

Множество современных методов в области анализа ПО практически невозможно реализовать без использования SMT-солверов. Несмотря на быстрый прогресс SMT-теории, использование солверов на практике часто затруднено различными очевидными и не очень очевидными проблемами. В докладе мы обсудим, что такое SMT-солверы (и, что более важно, чем они не являются), что им по силам, а что нет, как они могут быть использованы для конкретных задач и какие проблемы нужно преодолеть, чтобы они действительно заработали на практике.

Докладчик: Михаил Беляев, СПбПУ им. Петра Великого.