[Back]

J. Knoop, L. Kovacs, J. Zwirchmayr:
"Symbolic Loop Bound Computation for WCET Analysis";
Talk: 8th International Andrei Ershov Memorial Conference - Perspectives of System Informatics (PSI 2011), Akademgorodok, Novosibirsk, Russland; 2011-06-27 - 2011-07-01; in: "Ershov Informatic Conference, PSI Series, 8th Edition", Springer-Verlag, Lecture Notes in Computer Science, 7162 (2012), 224 - 239.

We present an automatic method for computing tight upper bounds
on the iteration number of special classes of program loops. These upper bounds are further used in the WCET analysis of programs. To do so, we refine program flows using SMT reasoning and rewrite multi-path loops into single-path ones.
Single-path loops are further translated into a set of recurrence relations over program variables. Recurrence relations are solved and iteration bounds of program loops are derived from the computed closed forms. For solving recurrences we deploy a pattern-based recurrence solving algorithm and compute closed forms
only for a restricted class of recurrence equations. However, in practice, these recurrences describe the behavior of a large set of program loops. Our technique is implemented in the r-TuBound tool and was successfully tried out on a number of challenging WCET benchmarks

WCET, loop bounds, upper bounds, SMT, program analysis

http://publik.tuwien.ac.at/files/PubDat_198261.pdf