Alternating Runtime and Size Complexity Analysis of Integer Programs

  • Marc Brockschmidt ,
  • Fabian Emmes ,
  • Stephan Falke ,
  • Carsten Fuhs ,
  • Juergen Giesl

TACAS |

We present a modular approach to automatic complexity analysis. Based on a novel alternation between finding symbolic time bounds for program parts and using these to infer size bounds on program variables, we can restrict each analysis step to a small part of the program while maintaining a high level of precision. Extensive experiments with the implementation of our method demonstrate its performance and power in comparison with other tools.