Computing a symbolic bound for a procedure

A method for computing a reachability bound on a control location inside a procedure that is executable by a processor in a computing device, wherein the method comprises:

• accessing a computer-readable medium to retrieve the procedure;
• generating a transition system with respect to the control location in the procedure, the transition system indicating, for each visit to the control location when the procedure is executed, how a variable is updated in an immediately subsequent visit to the control location when the procedure is executed;
• computing a symbolic bound with respect to the control location, wherein the symbolic bound is expressed in terms of inputs to the transition system;
• and
• translating the symbolic bound into the reachability bound, wherein the reachability bound is expressed in terms of inputs to the procedure.

A computer-readable memory comprising instructions that, when executed by a processor, cause the processor perform acts comprising:

• accessing a data repository to retrieve a procedure;
• generating a transition system with respect to a control location in the procedure, the transition system indicating, for each visit to the control location when the procedure is executed, how a variable is updated in an immediately subsequent visit to the control location when the procedure is executed;
• computing a bound with respect to the control location, wherein the bound is expressed in terms of inputs to the transition system, wherein the bound is computed based at least in part upon a ranking function of each transition in the transition system, and wherein the ranking function is computed based at least in part upon pattern-matching techniques;
• and translating the bound into a reachability bound, wherein the reachability bound is expressed in terms of inputs to the procedure, and wherein the reachability bound is indicative of a number of visits to the control location when the procedure is executed.