An Evaluation of WCET Analysis using Symbolic Loop Bounds
Jens Knoop, Laura Kovács, Jakob Zwirchmayr · Worst-Case Execution Time Analysis · 2011
In this paper we evaluate a symbolic loop bound generation technique recently proposed by the authors in [7]. The technique deploys pattern-based recurrence solving in conjunction with program flow refinement using SMT reasoning. The derived bounds are further used in the WCET analysis of programs with loops. This paper presents experimental evaluations of the method carried out with the r-TuBound software tool. We evaluate our method against various academic and industrial WCET benchmarks, and outline further challenges for symbolic loop bound computation.