**Date: **
17:00,
Thursday, November 3, 2016

**Speaker: **
Jan Strejček

**Venue: **IST Austria

**Notes: **

Thursday, 5pm, Mondi 3

Partial but Precise Loop Summarization and Its Applications

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.