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

В данной статье предлагается подход к аппроксимации функций, основанный на интерполяции Крейга, который лишен данного ограничения за счет усиления интерполяции при помощи случайной выборки моделей. При помощи поиска интересных взаимозависимостей между входными и выходными аргументами функции, случайная выборка моделей позволяет усилить совместные формулы до несовместных, тем самым делая возможным использование интерполяции Крейга. Результаты проведенных предварительных экспериментов подтверждают применимость данного подхода; в дальнейшем планируется провести более подробные исследования его характеристик на реальных примерах.