А, в этом плане. 😊
Тогда ещё Alloy можно вспомнить. При этом и тот, и другой с разными бэкендами ведут себя по-разному. Как минимум, разная производительность на одной и той же задаче.
Что только подтверждает мой тезис - на практике приходится затачиваться на особенности конкретного решателя или бэкенда.
Конечно, но сам по себе подход от ограничений и соотв. DSL — очень плодотворный.
В этом случае задача статического анализа представляет собой (1) порождение набора ограничений в результате обхода анализируемой программы. Этот набор — наша DSL-программа. А дальше (2) в дело вступают различные решатели, использование которых зависит от существа задачи: алгоритм для системы непересекающихся множеств (унификация), алгоритм достижения неподвижной точки (потоковый анализ), SMT-решатели и проч.
