For instance: Humanities and Science University Journal
About consortium subscription Contacts
(812) 4095364 Non-commercial partnership
St. Petersburg


"Humanities and Science University Journal" №8, 2014

Improving Static Analysis by Loop Unrolling on an Arbitrary Iteration

M. A. Belyaev, M. H. Akhin, V. M. Itsykson
Price: 50 руб.
 Program loops have proven to be a matter of great diffi culty for any method of static analysis or veri fi cation, because of the state space explosion and of the well-known halting problem that prevents us from reasoning about loop iteration counts in many
practical cases. In this paper we present an original approach to loop analysis for tools based on logic reasoning, e.g. bounded model checkers. It is based on unrolling loops not only from the beginning, but from the end or from any other loop iteration. Our approach has been implemented in the prototype bounded model checking tool called Borealis. Evaluation results on a number of test programs from NECLA and SV-COMP benchmarks show an over nine-fold increase in performance as well as some increase in analysis quality when using the presented approach.

program analysis, defect detection, loop unrolling, bounded model checking.
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.
Price: 50 рублей
To order