Abstract
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.
This work was supported in part by the Swiss NSF. The fourth author is supported by an FWF Hertha Firnberg Research grant (T425-N23).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
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)
Birkeland, B.: Calculus and Algebra with MathCad 2000. Haeftad. Studentlitteratur (2000)
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)
Danaila, I., Joly, P., Kaber, S.M., Postel, M.: An Introduction to Scientific Computing: Twelve Computational Projects Solved with MATLAB. Springer, Heidelberg (2007)
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)
Gosper, R.W.: Decision Procedures for Indefinite Hypergeometric Summation. PNAS 75, 40–42 (1978)
Graham, R.L., Knuth, D.E., Patashnik, O.: Concrete Mathematics, 2nd edn. Addison-Wesley Publishing Company, Reading (1989)
Gulwani, S., Jain, S., Koskinen, E.: Control-flow Refinement and Progress Invariants for Bound Analysis. In: Proc. of PLDI, pp. 375–385 (2009)
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)
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)
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)
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)
Hicklin, J., Moler, C., Webb, P., Boisvert, R.F., Miller, B., Pozo, R., Remington, K.: JAMA: A Java Matrix Package (2005), http://math.nist.gov/javanumerics/jama/
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)
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)
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)
Nemes, I., Petkovsek, M.: RComp: A Mathematica Package for Computing with Recursive Sequences. Journal of Symbolic Computation 20(5-6), 745–753 (1995)
Odersky, M.: The Scala Language Specification (2008), http://www.scala-lang.org
Prantl, A., Knoop, J., Schordan, M., Triska, M.: Constraint Solving for High-Level WCET Analysis. CoRR, abs/0903.2251 (2009)
Stewart, G.W.: JAMPACK: A Java Package For Matrix Computations, http://www.mathematik.hu-berlin.de/~lamour/software/JAVA/Jampack/
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)
Wolfram, S.: The Mathematica Book. Version 5.0. Wolfram Media, Champaign (2003)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Blanc, R., Henzinger, T.A., Hottelier, T., Kovács, L. (2010). ABC: Algebraic Bound Computation for Loops. In: Clarke, E.M., Voronkov, A. (eds) Logic for Programming, Artificial Intelligence, and Reasoning. LPAR 2010. Lecture Notes in Computer Science(), vol 6355. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17511-4_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-17511-4_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-17510-7
Online ISBN: 978-3-642-17511-4
eBook Packages: Computer ScienceComputer Science (R0)