Preview

Моделирование и анализ информационных систем

Расширенный поиск

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

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

Просмотров: 1011


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)