More Web Proxy on the site http://driver.im/

Article

ABC: algebraic bound computation for loops

Authors:

Thomas A. Henzinger,

Thibaud Hottelier,

Laura KovácsAuthors Info & Claims

LPAR'10: Proceedings of the 16th international conference on Logic for programming, artificial intelligence, and reasoning

Pages 103 - 118

Published: 25 April 2010 Publication History

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.

References

[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)

Digital Library

[2]

Birkeland, B.: Calculus and Algebra with MathCad 2000. Haeftad. Studentlitteratur (2000)

[3]

Cousot, P., Cousot, R.: Abstract Interpretation: a Unified LatticeModel for Static Analysis of Programs by Construction or Approximation of Fixpoints. In: Proc. of POPL, pp. 238-252 (1977)

Digital Library

[4]

Danaila, I., Joly, P., Kaber, S.M., Postel, M.: An Introduction to Scientific Computing: Twelve Computational Projects Solved with MATLAB. Springer, Heidelberg (2007)

[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)

[6]

Gosper, R.W.: Decision Procedures for Indefinite Hypergeometric Summation. PNAS 75, 40-42 (1978)

[7]

Graham, R.L., Knuth, D.E., Patashnik, O.: Concrete Mathematics, 2nd edn. Addison-Wesley Publishing Company, Reading (1989)

[8]

Gulwani, S., Jain, S., Koskinen, E.: Control-flow Refinement and Progress Invariants for Bound Analysis. In: Proc. of PLDI, pp. 375-385 (2009)

Digital Library

[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)

Digital Library

[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)

Digital Library

[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)

Digital Library

[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)

Digital Library

[13]

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/

[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)

Digital Library

[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)

Digital Library

[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)

Digital Library

[17]

Nemes, I., Petkovsek, M.: RComp: A Mathematica Package for Computing with Recursive Sequences. Journal of Symbolic Computation 20(5-6), 745-753 (1995)

Digital Library

[18]

Odersky, M.: The Scala Language Specification (2008), http://www.scala-lang.org

[19]

Prantl, A., Knoop, J., Schordan, M., Triska, M.: Constraint Solving for High-Level WCET Analysis. CoRR, abs/0903.2251 (2009)

[20]

Stewart, G.W.: JAMPACK: A Java Package For Matrix Computations, http://www.mathematik.hu-berlin.de/~lamour/software/JAVA/ Jampack/

[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)

Digital Library

[22]

Wolfram, S.: The Mathematica Book. Version 5.0. Wolfram Media, Champaign (2003)

Digital Library

Cited By

Kahn DHoffmann J(2021)Automatic amortized resource analysis with the Quantum physicist’s methodProceedings of the ACM on Programming Languages10.1145/34735815:ICFP(1-29)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473581
Wang DKahn DHoffmann J(2020)Raising expectations: automating expected cost analysis with typesProceedings of the ACM on Programming Languages10.1145/34089924:ICFP(1-31)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408992
Knoth TWang DPolikarpova NHoffmann JMcKinley KFisher K(2019)Resource-guided program synthesisProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314602(253-268)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314602
Show More Cited By

Recommendations

PS-ABC

A hybrid algorithm (PS-ABC) based on PSO and ABC is proposed.PS-ABC examines the aging degree of pbest to decide which type of search phase.Particle swarm optimization (PSO) serves as a local search phase.Onlooker and modified scout bee from the ABC ...
An upgraded artificial bee colony (ABC) algorithm for constrained optimization problems

Artificial bee colony (ABC) algorithm developed by Karaboga is a nature inspired metaheuristic based on honey bee foraging behavior. It was successfully applied to continuous unconstrained optimization problems and later it was extended to constrained ...
On ABC Estrada index of graphs
Abstract
Let G be a graph with vertex set V G = { v 1 , v 2 , … , v n } and edge set E G, and let d i be the degree of the vertex v i. The ABC matrix of G has the value ( d i + d j − 2 ) / ( d i d j ) if v i v j ∈ E G, and 0 otherwise, as its ( ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

LPAR'10: Proceedings of the 16th international conference on Logic for programming, artificial intelligence, and reasoning

April 2010

516 pages

ISBN:3642175104

Editors:
Edmund M. Clarke
Carnegie Mellon University, Computer Science Department, Pittsburgh, PA
,
Andrei Voronkov
University of Manchester, School of Computer Science, Manchester, UK

Sponsors

Office of Naval Research
Microsoft Research: Microsoft Research

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 25 April 2010

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

20
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Kahn DHoffmann J(2021)Automatic amortized resource analysis with the Quantum physicist’s methodProceedings of the ACM on Programming Languages10.1145/34735815:ICFP(1-29)Online publication date: 19-Aug-2021
https://dl.acm.org/doi/10.1145/3473581
Wang DKahn DHoffmann J(2020)Raising expectations: automating expected cost analysis with typesProceedings of the ACM on Programming Languages10.1145/34089924:ICFP(1-31)Online publication date: 3-Aug-2020
https://dl.acm.org/doi/10.1145/3408992
Knoth TWang DPolikarpova NHoffmann JMcKinley KFisher K(2019)Resource-guided program synthesisProceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3314221.3314602(253-268)Online publication date: 8-Jun-2019
https://dl.acm.org/doi/10.1145/3314221.3314602
Wang DHoffmann J(2019)Type-guided worst-case input generationProceedings of the ACM on Programming Languages10.1145/32903263:POPL(1-30)Online publication date: 2-Jan-2019
https://dl.acm.org/doi/10.1145/3290326
Ngo VCarbonneaux QHoffmann J(2018)Bounded expectations: resource analysis for probabilistic programsACM SIGPLAN Notices10.1145/3296979.319239453:4(496-512)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3296979.3192394
Ngo VCarbonneaux QHoffmann JFoster JGrossman D(2018)Bounded expectations: resource analysis for probabilistic programsProceedings of the 39th ACM SIGPLAN Conference on Programming Language Design and Implementation10.1145/3192366.3192394(496-512)Online publication date: 11-Jun-2018
https://dl.acm.org/doi/10.1145/3192366.3192394
Nguyen NTruong AThang HHu ZBui MSikdar BIDE IBinh HEngchuan WSang DOanh N(2017)A Compositional Type Systems for Finding Log Memory Bounds of Transactional ProgramsProceedings of the 8th International Symposium on Information and Communication Technology10.1145/3155133.3155183(409-416)Online publication date: 7-Dec-2017
https://dl.acm.org/doi/10.1145/3155133.3155183
Hoffmann JDas AWeng S(2017)Towards automatic resource bound analysis for OCamlACM SIGPLAN Notices10.1145/3093333.300984252:1(359-373)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3093333.3009842
Hoffmann JDas AWeng SCastagna GGordon A(2017)Towards automatic resource bound analysis for OCamlProceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages10.1145/3009837.3009842(359-373)Online publication date: 1-Jan-2017
https://dl.acm.org/doi/10.1145/3009837.3009842
Brockschmidt MEmmes FFalke SFuhs CGiesl J(2016)Analyzing Runtime and Size Complexity of Integer ProgramsACM Transactions on Programming Languages and Systems10.1145/286657538:4(1-50)Online publication date: 2-Aug-2016
https://dl.acm.org/doi/10.1145/2866575
Show More Cited By

View Options

View options

Media

Figures

Other

Tables

View Table of Contents