ABC: algebraic bound computation for loops. 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.
Keywords for this software
References in zbMATH (referenced in 7 articles )
Showing results 1 to 7 of 7.
- Hensel, Jera; Giesl, Jürgen; Frohn, Florian; Ströder, Thomas: Termination and complexity analysis for programs with bitvector arithmetic by symbolic execution (2018)
- Hoffmann, Jan; Das, Ankush; Weng, Shu-Chun: Towards automatic resource bound analysis for OCaml (2017)
- Sewell, Thomas; Kam, Felix; Heiser, Gernot: High-assurance timing analysis for a high-assurance real-time operating system (2017)
- Alves, Péricles R. O.; Rodrigues, Raphael E.; de Sousa, Rafael Martins; Quintão Pereira, Fernando Magno: A case for a fast trip count predictor (2015) ioport
- Knoop, Jens; Kovács, Laura; Zwirchmayr, Jakob: R-tubound: Loop bounds for WCET analysis (Tool paper) (2012) ioport
- Blanc, Régis; Henzinger, Thomas A.; Hottelier, Thibaud; Kovács, Laura: ABC: algebraic bound computation for loops (2010)
- Zwirchmayr, Jakob: Cutting-edge timing analysis techniques (2010)