LOOP ABSTRACTION FOR MODEL CHECKING

摘要

PROBLEM TO BE SOLVED: To provide systems and methods for abstracting a loop in a source code for model checking of the source code.SOLUTION: Loop abstraction includes determining (204) an original loop within a source code. The original loop includes a control statement and a loop body such that the original loop causes the loop body to be repeatedly executed based on the control statement. Further, output variables in the original loop and a number of blocks associated with the original loop are identified. The number of blocks is indicative of a count of unconditionally executed statement sets in which at least one output variable is computed. An abstract loop corresponding to the original loop is generated (208) by adding a modified expression for accelerated assignment for each output variable in a subset of the output variables, and replacing the control statement with a bounded control statement. The original loop is replaced (210) with the abstract loop for generating an abstract source code for model checking.