Bounding resource consumption using abstract interpretation

A method of statically computing a bound on the number of loop iterations or recursive procedure call invocations, the method comprising:

• instrumenting multiple counter variables in program code to count the number of units of resources utilized during execution of the code;
• determining invariants for the code based on program variables and the instrumented counter variables;
• existentially eliminating all program variables except counter variables and program inputs from the invariants;
• calculating respective bounds on the counter variables based on the invariants;
• and
• combining the respective bounds on the counter variables to generate the resource bound.

A system comprising:

• memory;
• one or more processors operatively coupled to the memory;
• an instrumentation module configured to:
• create copies of program input variables, introduce one or more counter variables in program code to count the number of loop iterations and/or recursive procedure call invocations, initialize the counter variables, increment the counter variables;
• and
• an abstract interpreter configured to:
• determine invariants for the program code involving both the counter variables and program variables, existentially eliminate all program variables except counter variables and program inputs from the invariants, and compute respective utilization bounds on the counter variables based on the invariants in terms of program input variables, according to a rule strategy.