Символьное исполнение в .NET: Автоматическое тестирование, верификация и синтез программ

В этом докладе вы узнаете про ближайшее будущее разработки, когда большая часть работы по тестированию и верификации программ будет происходить автоматически по щелчку мыши. Не все программисты любят писать юнит-тесты. Сложно их винить: творчества в этом процессе зачастую гораздо меньше, чем рутины. Можно ли сгенерировать все тесты автоматом и получить при этом стопроцентное покрытие?

Символьное исполнение — мощная техника анализа программ и генерации тестов, которая набирает популярность в последние годы. Мы погрузимся в теорию, которая стоит за Microsoft IntelliTest и поймём, как использовать символьное исполнение для ваших целей. Рассмотрим символьную виртуальную машину V# с примерами применения. Также получим знания о практическом применении базового элемента символьного исполнения — SMT-солвера. Мы увидим, как можно закодировать такие головоломки, как Судоку и Сапёр в несколько строк SMT-ограничений и попросим солвер их решить. Наконец, мы поговорим о приближающейся революции в разработке ПО, которая может изменить нашу профессию — о синтезе программ.