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.


Editor(s):
Clarke, Edmund M.
Voronkov, Andrei
Published in:
Logic for Programming, Artificial Intelligence, and Reasoning, 6355, 103-118
Presented at:
16th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Dakar, Senegal,, April 25–May 1, 2010
Year:
2010
Publisher:
Berlin, Heidelberg, Springer Berlin Heidelberg
Keywords:
Laboratories:




 Record created 2013-04-19, last modified 2018-09-13

Preprint:
Download fulltextPDF
Presentation slides:
Download fulltextPDF
Rate this document:

Rate this document:
1
2
3
 
(Not yet reviewed)