---
_id: '10908'
abstract:
- lang: eng
  text: 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.
acknowledgement: This work was supported in part by the Swiss NSF. The fourth author
  is supported by an FWF Hertha Firnberg Research grant (T425-N23).
article_processing_charge: No
author:
- first_name: Régis
  full_name: Blanc, Régis
  last_name: Blanc
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
- first_name: Thibaud
  full_name: Hottelier, Thibaud
  last_name: Hottelier
- first_name: Laura
  full_name: Kovács, Laura
  last_name: Kovács
citation:
  ama: '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>'
  apa: '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>'
  chicago: '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>.'
  ieee: '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.'
  ista: 'Blanc R, Henzinger TA, Hottelier T, Kovács L. 2010. ABC: Algebraic Bound
    Computation for loops. Logic for Programming, Artificial Intelligence, and Reasoning.
    LPAR: Conference on Logic for Programming, Artificial Intelligence and ReasoningLNCS
    vol. 6355, 103–118.'
  mla: '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>.'
  short: 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.
conference:
  end_date: 2010-05-01
  location: Dakar, Senegal
  name: 'LPAR: Conference on Logic for Programming, Artificial Intelligence and Reasoning'
  start_date: 2010-04-25
date_created: 2022-03-21T08:14:35Z
date_published: 2010-05-01T00:00:00Z
date_updated: 2022-06-13T07:44:21Z
day: '01'
department:
- _id: ToHe
doi: 10.1007/978-3-642-17511-4_7
editor:
- first_name: Edmund M
  full_name: Clarke, Edmund M
  last_name: Clarke
- first_name: Andrei
  full_name: Voronkov, Andrei
  last_name: Voronkov
intvolume: '      6355'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: https://infoscience.epfl.ch/record/186096
month: '05'
oa: 1
oa_version: Submitted Version
page: 103-118
place: Berlin, Heidelberg
publication: Logic for Programming, Artificial Intelligence, and Reasoning
publication_identifier:
  eisbn:
  - '9783642175114'
  eissn:
  - 1611-3349
  isbn:
  - '9783642175107'
  issn:
  - 0302-9743
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
series_title: LNCS
status: public
title: 'ABC: Algebraic Bound Computation for loops'
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 6355
year: '2010'
...