ABC: Algebraic Bound Computation for Loops

  • Régis Blanc
  • Thomas A. Henzinger
  • Thibaud Hottelier
  • Laura Kovács
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6355)


We present ABC, a software tool for automatically computing symbolic upper bounds on the number of iterations of nested program loops. The system combines static analysis of programs with symbolic summation techniques to derive loop invariant relations between program variables. Iteration bounds are obtained from the inferred invariants, by replacing variables with bounds on their greatest values. We have successfully applied ABC to a large number of examples. The derived symbolic bounds express non-trivial polynomial relations over loop variables. We also report on results to automatically infer symbolic expressions over harmonic numbers as upper bounds on loop iteration counts.


Iteration Variable Nest Loop Loop Iteration Abstract Interpretation Harmonic Number 
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.: Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis. In: Alpuente, M., Vidal, G. (eds.) SAS 2008. LNCS, vol. 5079, pp. 221–237. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  2. 2.
    Birkeland, B.: Calculus and Algebra with MathCad 2000. Haeftad. Studentlitteratur (2000)Google Scholar
  3. 3.
    Cousot, P., Cousot, R.: Abstract Interpretation: a Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proc. of POPL, pp. 238–252 (1977)Google Scholar
  4. 4.
    Danaila, I., Joly, P., Kaber, S.M., Postel, M.: An Introduction to Scientific Computing: Twelve Computational Projects Solved with MATLAB. Springer, Heidelberg (2007)CrossRefzbMATHGoogle Scholar
  5. 5.
    Ferdinand, C., Heckmann, R.: aiT: Worst Case Execution Time Prediction by Static Program Analysis. In: Proc. of IFIP Congress Topical Sessions, pp. 377–384 (2004)Google Scholar
  6. 6.
    Gosper, R.W.: Decision Procedures for Indefinite Hypergeometric Summation. PNAS 75, 40–42 (1978)MathSciNetCrossRefzbMATHGoogle Scholar
  7. 7.
    Graham, R.L., Knuth, D.E., Patashnik, O.: Concrete Mathematics, 2nd edn. Addison-Wesley Publishing Company, Reading (1989)zbMATHGoogle Scholar
  8. 8.
    Gulwani, S., Jain, S., Koskinen, E.: Control-flow Refinement and Progress Invariants for Bound Analysis. In: Proc. of PLDI, pp. 375–385 (2009)Google Scholar
  9. 9.
    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
  10. 10.
    Healy, C.A., Sjödin, M., Rustagi, V., Whalley, D.B., van Engelen, R.: Supporting Timing Analysis by Automatic Bounding of Loop Iterations. Real-Time Systems 18(2/3), 129–156 (2000)CrossRefGoogle Scholar
  11. 11.
    Henzinger, T.A., Hottelier, T., Kovacs, L.: Valigator: A Verification Tool with Bound and Invariant Generation. In: Cervesato, I., Veith, H., Voronkov, A. (eds.) LPAR 2008. LNCS (LNAI), vol. 5330, pp. 333–342. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  12. 12.
    Hermenegildo, M.V., Puebla, G., Bueno, F., Lopez-Garcia, P.: Integrated Program Debugging, Verification, and Optimization using Abstract Interpretation (and the Ciao System Preprocessor). Sci. Comput. Program. 58(1-2), 115–140 (2005)MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Hicklin, J., Moler, C., Webb, P., Boisvert, R.F., Miller, B., Pozo, R., Remington, K.: JAMA: A Java Matrix Package (2005),
  14. 14.
    Jost, S., Loidl, H., Hammond, K., Scaife, N., Hofmann, M.: “Carbon Credits” for Resource-Bounded Computations Using Amortised Analysis. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 354–369. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  15. 15.
    Müller-Olm, M., Petter, M., Seidl, H.: Interprocedurally Analyzing Polynomial Identities. In: Durand, B., Thomas, W. (eds.) STACS 2006. LNCS, vol. 3884, pp. 50–67. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  16. 16.
    Navas, J., Mera, E., Lopez-Garcia, P., Hermenegildo, M.V.: User-Definable Resource Bounds Analysis for Logic Programs. In: Dahl, V., Niemelä, I. (eds.) ICLP 2007. LNCS, vol. 4670, pp. 348–363. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  17. 17.
    Nemes, I., Petkovsek, M.: RComp: A Mathematica Package for Computing with Recursive Sequences. Journal of Symbolic Computation 20(5-6), 745–753 (1995)MathSciNetCrossRefzbMATHGoogle Scholar
  18. 18.
    Odersky, M.: The Scala Language Specification (2008),
  19. 19.
    Prantl, A., Knoop, J., Schordan, M., Triska, M.: Constraint Solving for High-Level WCET Analysis. CoRR, abs/0903.2251 (2009)Google Scholar
  20. 20.
    Stewart, G.W.: JAMPACK: A Java Package For Matrix Computations,
  21. 21.
    van Engelen, R.A., Birch, J., Gallivan, K.A.: Array Data Dependence Testing with the Chains of Recurrences Algebra. In: Proc. of IWIA, pp. 70–81 (2004)Google Scholar
  22. 22.
    Wolfram, S.: The Mathematica Book. Version 5.0. Wolfram Media, Champaign (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2010

Authors and Affiliations

  • Régis Blanc
    • 1
  • Thomas A. Henzinger
    • 2
  • Thibaud Hottelier
    • 3
  • Laura Kovács
    • 4
  1. 1.EPFLSwitzerland
  2. 2.ISTAustria
  3. 3.UCBerkeleyUSA
  4. 4.TUViennaAustria

Personalised recommendations