Ecole Polytechnique Fédérale de Lausanne
ABC Tool
english only

The ABC Tool

Short Description

ABC is a software tool for automatically computing tight symbolic upper bounds on the number of iterations and time complexities of a special class of loops, called the ABC-loops. These loops are nested for-loops such that each loop from the nested loop contains exactly one iteration variable with only one condition and (non-initializing) update on the iteration variable.

ABC stands for analyzing bound and complexity of loops. It combines static analysis of programs with symbolic summation techniques, and requires no user-guidance in providing additional set of predicates, templates and assertions. The derived bounds by ABC express polynomial relations over loop variables.

ABC is written in the SCALA programming language, and is based on the following three modules:

Registration and Legal Notices

The source code for the tool is password protected. To get the password send an email to Regis Blanc and/or Laura Kovács. It will be given for free to all researchers and non-commercial users.

Copyright © 2009 Regis Blanc, Laura Kovács — all rights reserved. Commercial use of the software is prohibited without prior written permission.


The tool is contained in the jar file and is accompanied by an introductory demo file

The results of applying ABC to some benchmark examples and JAMA loops are summarized in


To use the implementation it is sufficient to study the demo file above. It contains many examples to start with.

Further information can be found here:

R. Blanc, T. Henzinger, T. Hottelier and L. Kovács (2009), ABC: Analyzing Bounds and Complexities of Loops. Personal Communication, 2009. [pdf]

Versions and Bugs

The tool was developed by Regis Blanc at MTC, EPFL, Switzerland.

Right now you are using Version 0.1, last updated on July 15, 2009.

Please report any bugs and comments to Regis Blanc and/or Laura Kovács.

Developers Team