Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. ABC: Algebraic Bound Computation for Loops
 
conference paper

ABC: Algebraic Bound Computation for Loops

Blanc, Régis William  
•
Henzinger, Thomas A.  
•
Hottelier, Thibaud
Show more
Clarke, Edmund M.
•
Voronkov, Andrei
2010
Logic for Programming, Artificial Intelligence, and Reasoning
16th International Conference on 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.

  • Files
  • Details
  • Metrics
Type
conference paper
DOI
10.1007/978-3-642-17511-4_7
Author(s)
Blanc, Régis William  
Henzinger, Thomas A.  
Hottelier, Thibaud
Kovács, Laura
Editors
Clarke, Edmund M.
•
Voronkov, Andrei
Date Issued

2010

Publisher

Springer Berlin Heidelberg

Publisher place

Berlin, Heidelberg

Published in
Logic for Programming, Artificial Intelligence, and Reasoning
Series title/Series vol.

Lecture Notes in Computer Science

Volume

6355

Start page

103

End page

118

Subjects

loop invariants

•

symbolic computation

Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
MTC  
Event nameEvent placeEvent date
16th International Conference on Logic for Programming, Artificial Intelligence and Reasoning

Dakar, Senegal

April 25–May 1, 2010

Available on Infoscience
April 19, 2013
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/91657
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés