News and events archive
From the faculty
Informatics colloquium 7. 11. Loop summatization and its applicationsInformatics colloquium 7. 11. 2017, 14:00 lecture hall D2 doc. RNDr. Jan Strejček, Ph.D., FI MU Loop summatization and its applications Abstract: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.