Informatické kolokvium 7. 11. Loop summatization and its applications
Informatické kolokvium 7. 11. 2017, 14:00 posluchárna D2
doc. RNDr. Jan Strejček, Ph.D., FI MU
Loop summatization and its applications
Abstrakt: 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 when 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 a
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 other approaches.