Использование случайной выборки моделей для решения задачи интерполяции Крейга в рамках ограниченной проверки моделей
https://doi.org/10.18255/1818-1015-2014-6-7-17
Аннотация
Одной из самых сложных проблем при статическом анализе программ является анализ вызовов функций, также известный как межпроцедурный анализ. Классическим способом решения этой проблемы является подстановка тел функций в места вызовов, однако при этом значительно возрастает вычислительная сложность анализа из-за увеличения размера модели программы. Для решения этой проблемы можно использовать различные алгоритмы аппроксимации функций, которые заменяют полное тело функции на ее упрощенное описание, тем самым снижая сложность анализа. В контексте ограниченной проверки моделей в последнее время начала активно использоваться интерполяция Крейга, однако ее использование возможно только для пары несовместных логических формул.
В данной статье предлагается подход к аппроксимации функций, основанный на интерполяции Крейга, который лишен данного ограничения за счет усиления интерполяции при помощи случайной выборки моделей. При помощи поиска интересных взаимозависимостей между входными и выходными аргументами функции, случайная выборка моделей позволяет усилить совместные формулы до несовместных, тем самым делая возможным использование интерполяции Крейга. Результаты проведенных предварительных экспериментов подтверждают применимость данного подхода; в дальнейшем планируется провести более подробные исследования его характеристик на реальных примерах.
Об авторах
Марат Халимович АхинРоссия
исследователь, 195251, Россия, г. Санкт-Петербург, Политехническая ул., 29
Семен Леонидович Колтон
Россия
студент, 195251, Россия, г. Санкт-Петербург, Политехническая ул., 29
Владимир Михайлович Ицыксон
Россия
доцент, 195251, Россия, г. Санкт-Петербург, Политехническая ул., 29
Список литературы
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.
Рецензия
Для цитирования:
Ахин М.Х., Колтон С.Л., Ицыксон В.М. Использование случайной выборки моделей для решения задачи интерполяции Крейга в рамках ограниченной проверки моделей. Моделирование и анализ информационных систем. 2014;21(6):7-17. https://doi.org/10.18255/1818-1015-2014-6-7-17
For citation:
Akhin M., Kolton S., Itsykson V. Random Model Sampling: Making Craig Interpolation Work When It Should Not. Modeling and Analysis of Information Systems. 2014;21(6):7-17. (In Russ.) https://doi.org/10.18255/1818-1015-2014-6-7-17