1. Evaluation on Real World C Code
Details on our first experiment are available here.
2. Evaluation on Examples from the Literature
Our benchmark and the input files for the different tools are available here. The README file describes how the inputs for the different tools where generated.
The file names tell where the respective example was taken from:
- ABC_* are the examples from the evaluation of
ABC: Algebraic Loop Bound Computation, LPAR'09
- C4B_* are the examples from the evaluation of
Compositional Certified Resource Bounds, PLDI'15
(we did not add the md5sum example because it has multiple functions, we did not add the quicksort example because its recursive, the SPEED examples are named starting with SPEED_*)
- KoAT-2013_* are the example from the paper
Alternating Runtime and Size Complexity Analysis of Integer Programs, TACAS'14
- Loopus* are the examples from the papers
- Bound Analysis of Imperative Programs with the Size-change Abstraction, SAS'10
- A Simple and Scalable Static Analysis for Bound Analysis and Amortized Complexity Analysis, CAV'14
- and of our JAR submission
- Rank-2010* are the examples from the paper
Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs, SAS'10
- SPEED* are the examples from various papers of the SPEED project
- WTC_* are the examples from the evaluation of Multi-dimensional Rankings, Program Termination, and Complexity Bounds of Flowchart Programs, SAS'10
3. Evaluation on Challenging Loop Iteration Patterns
Our benchmark is available here.
Look here for the current version of loopus.