conference paper published yes Régis Blanc author Thomas A Henzinger author 40876CD8-F248-11E8-B48F-1D18A9856A870000-0002-2985-7724 Thibaud Hottelier author Laura Kovács author Edmund MClarke editor AndreiVoronkov editor ToHe department LPAR: Logic for Programming, Artificial Intelligence and Reasoning 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. Springer Nature2010Dakar, Senegal eng 0302-9743 1611-3349 9783642175107 00030966800000710.1007/978-3-642-17511-4_7 6355103-118 Blanc R, Henzinger TA, Hottelier T, Kovács L. ABC: Algebraic Bound Computation for loops. In: Clarke EM, Voronkov A, eds. <i>Logic for Programming, Artificial Intelligence, and Reasoning</i>. Vol 6355. LNCS. Berlin, Heidelberg: Springer Nature; 2010:103-118. doi:<a href="https://doi.org/10.1007/978-3-642-17511-4_7">10.1007/978-3-642-17511-4_7</a> Blanc R, Henzinger TA, Hottelier T, Kovács L. 2010. ABC: Algebraic Bound Computation for loops. Logic for Programming, Artificial Intelligence, and Reasoning. LPAR: Logic for Programming, Artificial Intelligence and ReasoningLNCS vol. 6355, 103–118. Blanc, R., Henzinger, T. A., Hottelier, T., &#38; Kovács, L. (2010). ABC: Algebraic Bound Computation for loops. In E. M. Clarke &#38; A. Voronkov (Eds.), <i>Logic for Programming, Artificial Intelligence, and Reasoning</i> (Vol. 6355, pp. 103–118). Berlin, Heidelberg: Springer Nature. <a href="https://doi.org/10.1007/978-3-642-17511-4_7">https://doi.org/10.1007/978-3-642-17511-4_7</a> R. Blanc, T. A. Henzinger, T. Hottelier, and L. Kovács, “ABC: Algebraic Bound Computation for loops,” in <i>Logic for Programming, Artificial Intelligence, and Reasoning</i>, Dakar, Senegal, 2010, vol. 6355, pp. 103–118. Blanc, Régis, et al. “ABC: Algebraic Bound Computation for Loops.” <i>Logic for Programming, Artificial Intelligence, and Reasoning</i>, edited by Edmund M Clarke and Andrei Voronkov, vol. 6355, Springer Nature, 2010, pp. 103–18, doi:<a href="https://doi.org/10.1007/978-3-642-17511-4_7">10.1007/978-3-642-17511-4_7</a>. Blanc, Régis, Thomas A Henzinger, Thibaud Hottelier, and Laura Kovács. “ABC: Algebraic Bound Computation for Loops.” In <i>Logic for Programming, Artificial Intelligence, and Reasoning</i>, edited by Edmund M Clarke and Andrei Voronkov, 6355:103–18. LNCS. Berlin, Heidelberg: Springer Nature, 2010. <a href="https://doi.org/10.1007/978-3-642-17511-4_7">https://doi.org/10.1007/978-3-642-17511-4_7</a>. R. Blanc, T.A. Henzinger, T. Hottelier, L. Kovács, in:, E.M. Clarke, A. Voronkov (Eds.), Logic for Programming, Artificial Intelligence, and Reasoning, Springer Nature, Berlin, Heidelberg, 2010, pp. 103–118. 109082022-03-21T08:14:35Z2025-09-30T09:51:13Z