Complexity and Resource Bound Analysis of Imperative Programs using Difference Constraints

Details on the Experimental Evaluation

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.