Symbolic Loop Bound Computation for WCET Analysis

  • Jens Knoop
  • Laura Kovács
  • Jakob Zwirchmayr
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7162)


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.


Recurrence Equation Computer Algebra System Loop Iteration Abstract Interpretation Simple Loop 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Albert, E., Arenas, P., Genaim, S., Puebla, G.: Closed-Form Upper Bounds in Static Cost Analysis. J. Automated Reasoning 46(2), 161–203 (2011)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Ammarguellat, Z., Harrison III., W.L.: Automatic Recognition of Induction Variables and Recurrence Relations by Abstract Interpretation. In: Proc. of PLDI, pp. 283–295 (1990)Google Scholar
  3. 3.
    Blanc, R., Henzinger, T.A., Hottelier, T., Kovács, L.: ABC: Algebraic Bound Computation for Loops. In: Clarke, E.M., Voronkov, A. (eds.) LPAR-16 2010. LNCS, vol. 6355, pp. 103–118. Springer, Heidelberg (2010)CrossRefGoogle Scholar
  4. 4.
    Brummayer, R., Biere, A.: Boolector: An Efficient SMT Solver for Bit-Vectors and Arrays. In: Kowalewski, S., Philippou, A. (eds.) TACAS 2009. LNCS, vol. 5505, pp. 174–177. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  5. 5.
    Everest, G., van der Poorten, A., Shparlinski, I., Ward, T.: Recurrence Sequences. Mathematical Surveys and Monographs, vol. 104. American Mathematical Society (2003)Google Scholar
  6. 6.
    Gulwani, S., Mehra, K.K., Chilimbi, T.M.: SPEED: Precise and Efficient Static Estimation of Program Computational Complexity. In: Proc. of POPL, pp. 127–139 (2009)Google Scholar
  7. 7.
    Gulwani, S., Zuleger, F.: The Reachability-Bound Problem. In: Proc. of PLDI, pp. 292–304 (2010)Google Scholar
  8. 8.
    Gustafsson, J., Ermedahl, A., Sandberg, C., Lisper, B.: Automatic Derivation of Loop Bounds and Infeasible Paths for WCET Analysis Using Abstract Execution. In: Proc. of RTSS, pp. 57–66 (2006)Google Scholar
  9. 9.
    Henzinger, T., Hottelier, T., Kovács, L.: Valigator: A Verification Tool with Bound and Invariant Generation. In: Proc. of LPAR-15, pp. 333–342 (2008)Google Scholar
  10. 10.
    Holsti, N., Gustafsson, J., Bernat, G., Ballabriga, C., Bonenfant, A., Bourgade, R., Cassé, H., Cordes, D., Kadlec, A., Kirner, R., Knoop, J., Lokuciejewski, P., Merriam, N., de Michiel, M., Prantl, A., Rieder, B., Rochange, C., Sainrat, P., Schordan, M.: WCET 2008 - Report from the Tool Challenge 2008 - 8th Intl. Workshop on Worst-Case Execution Time (WCET) Analysis. In: Proc. of WCET (2008)Google Scholar
  11. 11.
    Kauers, M.: SumCracker: A Package for Manipulating Symbolic Sums and Related Objects. J. of Symbolic Computation 41(9), 1039–1057 (2006)MathSciNetzbMATHCrossRefGoogle Scholar
  12. 12.
    Kirner, R., Knoop, J., Prantl, A., Schordan, M., Kadlec, A.: Beyond Loop Bounds: Comparing Annotation Languages for Worst-Case Execution Time Analysis. J. of Software and System Modeling (2010); Online editionGoogle Scholar
  13. 13.
    de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  14. 14.
    Lisper, B.: Fully Automatic, Parametric Worst-Case Execution Time Analysis. In: Proc. of WCET, pp. 99–102 (2003)Google Scholar
  15. 15.
    Michiel, M.D., Bonenfant, A., Cassé, H., Sainrat, P.: Static Loop Bound Analysis of C Programs Based on Flow Analysis and Abstract Interpretation. In: Proc. of RTCSA, pp. 161–166 (2008)Google Scholar
  16. 16.
    Paule, P., Schorn, M.: A Mathematica Version of Zeilberger’s Algorithm for Proving Binomial Coefficient Identities. J. of Symbolic Computation 20(5-6), 673–698 (1995)MathSciNetzbMATHCrossRefGoogle Scholar
  17. 17.
    Prantl, A.: High-level Compiler Support for Timing-Analysis. PhD thesis, Vienna University of Technology (2010)Google Scholar
  18. 18.
    Prantl, A., Knoop, J., Kirner, R., Kadlec, A., Schordan, M.: From Trusted Annotations to Verified Knowledge. In: Proc. of WCET, pp. 39–49 (2009)Google Scholar
  19. 19.
    Prantl, A., Knoop, J., Schordan, M., Triska, M.: Constraint Solving for High-Level WCET Analysis. In: Proc. of WLPE, pp. 77–89 (2008)Google Scholar
  20. 20.
    Prantl, A., Schordan, M., Knoop, J.: TuBound - A Conceptually New Tool for WCET Analysis. In: Proc. of WCET, pp. 141–148 (2008)Google Scholar
  21. 21.
    Riazanov, A., Voronkov, A.: The Design and Implementation of Vampire. AI Communications 15(2-3), 91–110 (2002)zbMATHGoogle Scholar
  22. 22.
    Schneider, C.: Symbolic Summation with Single-Nested Sum Extensions. In: Proc. of ISSAC, pp. 282–289 (2004)Google Scholar
  23. 23.
    Wolfram, S.: The Mathematica Book. Version 5.0. Wolfram Media (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Jens Knoop
    • 1
  • Laura Kovács
    • 1
  • Jakob Zwirchmayr
    • 1
  1. 1.Vienna University of TechnologyAustria

Personalised recommendations