A system for loop abstraction in a source code, for model checking of the source code, the system comprising a processor coupled to a memory, and the processor executes plurality of modules stored in the memory 108, wherein the plurality of modules comprising: a context expansion module coupled to the processor 104 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; and identify output variables in the original loop and a number of blocks associated with the original loop, wherein the output variables comprises one or more input-output variables and one or more pure output variables, wherein the one or more input-output variables are indicative of the output variables read and modified in the original loop, and the one or more pure output variables are indicative of the output variables modified without being read in the original loop, and wherein the block is an unconditionally executed set of statements associated with the original loop within the source code, and the number of blocks is indicative of the blocks where a unique set of output variables is modified; and a loop abstraction module coupled to the processor to generate an abstract loop corresponding to the original loop when a property or a condition associated with the source code, which is to be verified during the model checking of the source code, is placed outside 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 input-output variable in the original loop, wherein the modified expression is added before the loop body; and replace the control statement with a bounded control statement, in order to transform the original loop to the abstract loop, wherein the bounded control statement includes an upper bound based on the number of blocks and a count of the pure output variables in the original loop; and replace the original loop with the abstract loop in the source code to generate an abstract source code for model checking of the source code; and a model checker module coupled to the processor to perform the model checking of the abstract source code to verify the property or condition of the source code. a context expansion module coupled to the processor 104 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; and identify output variables in the original loop and a number of blocks associated with the original loop, wherein the output variables comprises one or more input-output variables and one or more pure output variables, wherein the one or more input-output variables are indicative of the output variables read and modified in the original loop, and the one or more pure output variables are indicative of the output variables modified without being read in the original loop, and wherein the block is an unconditionally executed set of statements associated with the original loop within the source code, and the number of blocks is indicative of the blocks where a unique set of output variables is modified; and a loop abstraction module coupled to the processor to generate an abstract loop corresponding to the original loop when a property or a condition associated with the source code, which is to be verified during the model checking of the source code, is placed outside 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 input-output variable in the original loop, wherein the modified expression is added before the loop body; and replace the control statement with a bounded control statement, in order to transform the original loop to the abstract loop, wherein the bounded control statement includes an upper bound based on the number of blocks and a count of the pure output variables in the original loop; and replace the original loop with the abstract loop in the source code to generate an abstract source code for model checking of the source code; and add a modified expression for accelerated assignment of each input-output variable in the original loop, wherein the modified expression is added before the loop body; and replace the control statement with a bounded control statement, in order to transform the original loop to the abstract loop, wherein the bounded control statement includes an upper bound based on the number of blocks and a count of the pure output variables in the original loop; and replace the original loop with the abstract loop in the source code to generate an abstract source code for model checking of the source code; and a model checker module coupled to the processor to perform the model checking of the abstract source code to verify the property or condition of the source code.