М. А. Беляев, М. Х. Ахин, В. М. Ицыксон
Цена: 50 руб.
Анализ циклов представляет собой крайне сложную задачу в рамках статического анализа или верификации из-за проблемы взрыва пространства состояний и неразрешимости проблемы останова, что не позволяет статически определить возможное число итераций циклов. В данной статье предлагается подход к анализу циклов для инструментов, основанных на логическом выводе, например, для средств ограниченной проверки моделей. Подход основывается на раскрутке циклов не только с начала, а и на любой произвольной итерации. Экспериментальные исследования предложенного подхода на наборе тестовых программ NECLA и SV-COMP показали более чем девятикратное увеличение
производительности, а также определенное улучшение качества анализа.
Ключевые слова: анализ программ, поиск дефектов, раскрутка циклов, ограниченная проверка моделей.
REFERENCES
1. Aho, A.V. et al. Compilers: principles, techniques & tools. 2007, Pearson
Education India.
2. Aiken, A. et al. An overview of the Saturn project. 2007. Pp. 43–48.
3. Akhin, M. et al. Yet another defect detection: Combining bounded model checking
and code contracts. 2013. Pp. 1–11.
4. Ball, T. et al. Leaping loops in the presence of abstraction. Computer aided
veri fi cation. 2007, Springer Berlin Heidelberg. Pp. 491–503.
5. Beizer, B. Software testing techniques. 2003, Dreamtech Press.
6. Beyer, D. Competition on software veri fi cation. 2012, Springer. Pp. 504–524.
7. Biere, A. et al. Symbolic model checking without BDDs. 1999. Pp. 193–207.
8. Blass, A. & Gurevich, Y. Inadequacy of computable loop invariants. ACM
Transactions on Computational Logic (TOCL). 2001, 2, 1. Pp. 1–11.
9. Clarke, E. et al. A tool for checking ANSI-C programs. 2004. Pp. 168–176.
10. Godefroid, P. & Luchaup, D. Automatic partial loop summarization in dynamic
test generation. 2011, New York, USA. Pp. 23–33.
11. Ivančić, F. and Sankaranarayanan, S. NECLA static analysis benchmarks.
12. Jaffar, J. et al. Unbounded symbolic execution for program veri fi cation. 2012,
Berlin, Heidelberg. Pp. 396–411.
13. Kroening, D. et al. Under-approximating loops in C programs for fast
counterexample detection. Computer aided verification. 2013, Springer Berlin
Heidelberg. Pp. 381–396.
14. Kroening, D. et al. Loop summarization using abstract transformers. Automated
technology for veri fi cation and analysis. 2008, Springer. Pp. 111–125.
15. Lattner, C. and Adve, V. LLVM: A compilation framework for lifelong program
analysis & transformation. 2004. Pp. 75–86.
16. Merz, F. et al. LLBMC: Bounded model checking of C and C++ programs using
a compiler IR. 2012. Pp. 146–161.
17. Novillo, D. Tree SSA: A new optimization infrastructure for GCC. Proceedings
of the 2003 GCC developers’ summit. 2003. Pp. 181–193.
18. Pop, S. et al. Induction variable analysis with delayed abstractions. High
performance embedded architectures and compilers. 2005, Springer. Pp. 218–232.
19. Saxena, P. et al. Loop-extended symbolic execution on binary programs. 2009,
New York, USA. Pp. 225–236.
20. Strejček, J. & Trtík, M. Abstracting path conditions. 2012, New York, USA.
Pp. 155–165.
21. Xiao, X. et al. Characteristic studies of loop problems for structural test
generation via symbolic execution. 2013, Palo Alto, California.
