Использование случайной выборки моделей для решения задачи интерполяции Крейга в рамках ограниченной проверки моделей

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

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

1. Marat Akhin, Mikhail Belyaev, and Vladimir Itsykson. Yet another defect detection: Combining bounded model checking and code contracts // PSSV’13. 2013. P. 1–11.

2. Armin Biere, Alessandro Cimatti, Edmund M. Clarke, and Yunshan Zhu. Symbolic model checking without BDDs // TACAS’99. 1999. P. 193–207.

3. J¨urgen Christ, Jochen Hoenicke, and Alexander Nutz. SMTInterpol: An interpolating SMT solver // SPIN’12. 2012. P. 248–254.

4. Alessandro Cimatti, Alberto Griggio, Bastiaan Joost Schaafsma, and Roberto Sebastiani. The MathSAT5 SMT solver // TACAS’13. 2013. P. 93–107.

5. Edmund Clarke, Orna Grumberg, Somesh Jha, Yuan Lu, and Helmut Veith. Counterexample-guided abstraction refinement for symbolic model checking // The Journal of ACM. Sep. 2003. 50(5). P. 752–794.

6. William Craig. Three uses of the Herbrand-Gentzen theorem in relating model theory and proof theory // The Journal of Symbolic Logic. Sep 1957. 22(3). P. 269–285.

7. Isil Dillig, Thomas Dillig, Boyang Li, and Ken McMillan. Inductive invariant generation via abductive inference // OOPSLA’13. P. 443–456. New York, USA, 2013. ACM.

8. Franjo Ivanˇci´c and Sriram Sankaranarayanan. NECLA static analysis benchmarks. http://www.nec-labs.com/research/system/systems_SAV-website/benchmarks.php

9. Boyang Li, Isil Dillig, Thomas Dillig, Ken McMillan, and Mooly Sagiv. Synthesis of circular compositional program proofs via abduction // TACAS’13. 2013. P. 370–384.

10. K. L. McMillan. Applications of Craig interpolants in model checking // TACAS’05. 2005. P. 1–12.

11. K. L. McMillan. Lazy abstraction with interpolants // CAV’06. 2006. P. 123–136.

12. K. L. McMillan. Interpolants from Z3 proofs // FMCAD ’11. 2011. P. 19–27.

13. Ondrej Sery, Grigory Fedyukovich, and Natasha Sharygina. Interpolation-based function summaries in bounded model checking // HVC’11. 2012. P. 160–175.