Очередная работа от John Regehr со товарищи на тему супероптимизации.

Dataflow-based Pruning for Speeding up Superoptimization
https://www.cs.utah.edu/~regehr/dataflow-pruning.pdf

Заметно, как первая эйфория от полностью автоматического применения SMT-решателя и метода CEGIS уходит. Оказывается, для задач реалистичных размерностей все равно приходится придумывать если не полностью собственную процедуру поиска с учетом эвристик из предметной области, то хотя бы ее элементы -- иначе SMT-решателю справиться будет тяжело.

Ключевая идея авторов -- прежде чем передавать на вход SMT-решателю очередную программу-кандидат из пространства поиска, полезно эту недооформленную программу (описывающую целое семейство конкретных программ) проверить на соответствие спецификации с помощью абстрактной интерпретации (анализ потоков данных на предмет known bits, int. ranges и так далее). В том числе, на конкретных тестовых входах.

В завершающей части статьи есть краткий и полезный обзор современного положения дел в области синтеза программ.

#smt #analysis #synthesis