LOOP ABSTRACTION FOR MODEL CHECKING

摘要

Loop abstraction includes determining an original loop within the 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 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 with the abstract loop for generating an abstract source code for the model checking.

主权项

1. A system for loop abstraction in a source code, for model checking of the source code, the system comprising:
a context expansion module coupled to the processor to,
receive the source code for abstraction;determine an original loop within the source code, wherein the original loop includes a control statement and a loop body, wherein the original loop causes the loop body to be repeatedly executed based on the control statement; andidentify output variables in the original loop and a number of blocks associated with the original loop, wherein the number of blocks is indicative of a count of unconditionally executed statement sets in which at least one output variable is computed; and a loop abstraction module coupled to the processor to generate an abstract loop corresponding to the original loop, wherein to generate the abstract loop the loop abstraction module is further configured to:
add a modified expression for accelerated assignment of each output variable in a first subset of the output variables, wherein the modified expression is added before the loop body; andreplace the control statement with a bounded control statement, wherein the bounded control statement includes an upper bound based on the number of blocks and count of a second subset of the output variable; andreplace the original loop with the abstract loop to generate an abstract source code for the model checking.