Jan Strejček

Date: 17:00, Thursday, November 3, 2016
Speaker: Jan Strejček
Venue: IST Austria

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.

Posted in RiSE Seminar