Partial but Precise Loop Summarization and Its Applications
Jan Strejcek, Masaryk University
We show a symbolic-execution-based algorithm computing the precise effect of a program cycle on program variables. For a program variable, the algorithm produces an expression representing the variable value after the number of cycle iterations specified by parameters of the expression. The algorithm is partial in the sense that it can fail to find such an expression for some program variables (for example, it fails in cases where the variable value depends on the order of paths in the cycle taken during iterations).
We present two applications of this loop summarization procedure. The
first is the construction of a nontrivial necessary condition on program
input to reach a given program location. The second application is a
loop bound detection algorithm, which produces tighter loop bounds than
Jan Strejcek is an associate professor at the Faculty of Informatics
of Masaryk University located in Brno, Czech Republic. He received his
PhD in Computer Science (2005) and Master degrees in Mathematics
(2000) and Computer Science (2001) from the same university. His
current research focuses on automata over infinite words, automatic
program analysis, and SMT-solving of quantified bitvector formulae.