FORM2 THEPATENTS ACT, 1970 (39 of 1970) & THEPATENTS RULES, 2003 COMPLETE SPECIFICATION (See section 10, rule 13) 1. Title of the invention: LOOP ABSTRACTION FOR MODEL CHECKING 2. Applicant(s) NAME NATIONALITY ADDRESS TATA CONSULTANCY SERVICES LIMITED Indian Nirmal Building, 9th Floor, Nariman Point, Mumbai, Maharashtra 400021, India 3. Preamble to the description COMPLETE SPECIFICATION The following specification particularly describes the invention and the manner in which it is to be performed. FIELD OF INVENTION [0001] The present subject matter relates to data abstraction for model checking and, particularly but not exclusively, to loop abstraction in a computer 5 program for model checking. BACKGROUND [0002] A computer program is a sequence of codes written in a programming language to perform a specified task in a computing device, such as a computer and a laptop. The computer program, also referred to as a program, usually includes one or 10 more execution statements that are executed for performing the specified task. The statements are generally provided in a sequential form with the program execution beginning from execution of a first statement and ending with execution of a last statement. However, in complex programs, the statements may be provided in the form of loops such that a particular set of statements is executed in a given sequence 15 repeatedly until a loop termination condition is reached. On execution of the last sequential statement in such cases, it is first determined whether the termination condition has been achieved or not. If the termination condition is not achieved, the given sequence starting from the first statement is executed again, otherwise the loop in the program is terminated. Further, a loop may be configured to run for a specified 20 loop bound. The loop bounds may be understood as the maximum number of times a loop has to be executed. BRIEF DESCRIPTION OF THE DRAWINGS [0003] The detailed description is described with reference to the accompanying figure(s). In the figure(s), the left-most digit(s) of a reference number 25 identifies the figure in which the reference number first appears. The same numbers are used throughout the figure(s) to reference like features and components. Some 3 implementations of systems and/or methods in accordance with implementations of the present subject matter are now described, by way of example, and with reference to the accompanying figure(s), in which: [0004] Fig. 1 illustrates a network environment implementing a loop 5 abstraction system, according to an implementation of the present subject matter. [0005] Fig. 2 illustrates a method for abstracting a loop in a source code, according to an implementation of the present subject matter. 10 DETAILED DESCRIPTION [0006] While executing programs having loops, errors may be encountered in cases of indefinite loops or loops having large loop bounds. Generally, in order to ensure error free execution of the program, the program is initially checked for errors, for example, by a program analyzer or a model checker of the computer device. The 15 model checker is configured to analyze the program and check for various errors that may occur on execution of the program. However, for the loops with nondeterministic bounds i.e. indefinite or large loop bounds, the model checker ascertains a small upper bound and unrolls the loops in accordance with the upper bound. Further, ascertaining the upper bound may be a time consuming and difficult task for 20 the model checker as the model checker may lack sufficient intelligence for ascertaining such a bound. Thus, providing an inadequate, i.e., a smaller bound than required may cause a bounded model checker to produce results, such as a loop unrolling assertion failure. Additionally, in both the cases of a smaller bound and a larger bound the model checker may produce an “out of memory” failure. Therefore 25 it may not be feasible to verify loops having indefinite or large bounds using a bounded model checker. [0007] Other conventional techniques involve loop abstraction for model checking and verification. One such approach relates to loop abstraction based on 4 number of transitions that a loop goes through. Abstracting loops based on the number of transitions may however not be efficient for indefinite loops as in such cases the number of transitions may not be determined accurately, thus affecting the efficiency of model checking. 5 [0008] Another conventional technique of loop abstraction involves unrolling a given loop twice. Initially, the given loop is unrolled n number of times followed by resetting all variables updated in the loop body during the unrolling. The loop is subsequently unrolled m number of times. However, using the present technique may not be useful for verifying certain loops having complex conditions as all the 10 variables updated during loop unrolling are not reset in each iteration of the loop unrolling, thus affecting subsequent unrolling. Further, the value of m is a configurable parameter and is not evaluated for efficiency. The model checker may thus either run out of memory or cause loop unwinding assertion failures. [0009] Yet another conventional technique involves predicate abstraction for 15 verification. The predicate abstraction typically involves mapping concrete data types to abstract data types through predicates over the concrete data. However, using predicate abstraction for large programs may be infeasible due to the computational costs associated with the technique. [0010] Thus, in the process of verification of computer programs with loops 20 having non-deterministic bounds, a need for an efficient and lesser time consuming mechanism to abstract the loops with non-deterministic bound without memory or processing errors exists. [0011] According to an implementation of the present subject matter, systems and methods for abstracting a loop in a source code for model checking of the source 25 code are described. The source code may be understood as a computer program written in a programming language. The systems and methods can be implemented in a variety of computing devices. The computing devices include, but are not limited 5 to, desktop computers, hand-held devices, laptops or other portable computers, and the like. In one implementation, the systems and methods implementing loop abstraction may be provided for loop abstraction and subsequent model checking in programs written using programming languages including, but not limited to, C, C++, 5 VC++, C#, and the like. [0012] In one implementation, the source code received for abstraction may be analyzed to determine an original loop having a loop body and a control statement. Further, output variables and number of blocks associated with the original loop are also identified. Furthermore, an abstract loop corresponding to the original loop may 10 be generated. For this, a modified expression for accelerated assignment of each output variable in a first subset of the output variables is added before the loop body. Additionally, the loop control statement may be replaced with a bounded control statement which includes the loop control statement. Further, a count of a second subset output variable may also be considered for bounded control statement. The 15 method further replaces the original loop with the abstract loop to generate an abstract source code for model checking. Here, the first subset of the output variable corresponds to input-output variables (IO) and the second subset of the output variable corresponds to pure output variables. [0013] The control statement in the original loop may be understood as the 20 termination condition for the original loop. The original loop can include a plurality of variables that may be read, used, or modified during loop execution. The loop variables may be further classified as input variables, pure output variables, and input-output (IO) variables. The input variables are the variables that are read only, i.e., just provide input to the original loop, and are thus not modified during loop 25 execution. The pure output variables on the other hand are the ones that are only modified during the loop execution and also used outside the loop. The IO variables are the ones that are used for providing input and are modified during the loop execution. 6 [0014] In one implementation, a loop in a computer program, such as C Program, is abstracted. In order to abstract the loop in the computer program, each property to be verified, referred to as ‘a’, can be determined and may be modelled as an assertion. Further, the computer program is sliced with respect to the property ‘a’ 5 and the reduced sliced computer program is used for verification of the property ‘a’. Further, an iterative context expansion module verifies the property ‘a’ of the computer program. In the verification process, a function ‘f’ in which assertion ‘a’ lies is selected as the starting context for analysis of the computer program. Furthermore, loops with large and unknown bounds from the function ‘f’ are 10 abstracted and the abstracted computer program is analyzed using a model checker. If the model checker reports the property ‘a’ of the computer program as safe then it can safely conclude that the property ‘a’ is safe in the computer program. If the model checker reports the property ‘a’ of the computer program as unsafe then the context is widened to the functions that call ‘f’. The model checker reporting process is repeated 15 until either the property ‘a’ of the computer program is proved to be safe or the model checker does not scale up or the property ‘a’ of the computer program is proved to be unsafe at the top level function. [0015] Further, the present loop abstraction process uses loop replacement to transform loops with large or unknown bounds when the assertion is outside the loop 20 body of the computer program and uses induction when the assertion is within the loop body of the computer program. Also, nested loops of the computer program are abstracted starting from the innermost loop body and proceeding to the outermost loop body of the computer program. According to an implementation, flags can be used to determine if the assertion is present inside the loop body or outside it. 25 [0016] Further, in both transformations, each IO variable is abstracted by assigning a non-deterministic value to it at the start of the abstract loop. An IO variable is a variable that is first read and then modified along some path of the loop body. For a variable that participates in a linear recurrence equation, the non7 deterministic assignment to it is the closed form acceleration for a non-deterministic number of iterations of its assignment. Mutual recurrences are also handled similarly, when more than one recurrent variable have mutual dependency. [0017] The systems and methods of the present subject matter thus facilitate in implementing loo 5 p abstraction process in a program. The original loop is replaced by another loop which has a small known bound which ensures that the loop is executed only a fixed number of times thus reducing the costs associated with memory resource, processing resource, and time consumption and errors, such as memory overflow or loop unwinding assertion failures caused due to execution of 10 loops having indefinite or large loop bounds. Further, the computer program may be abstracted into another computer program which allows all runs of the original computer program along with additional runs. Such an abstracted computer program may be called as an over-approximation of the original computer program. Therefore, if a property of the computer program is valid in the abstracted computer program, 15 then it will also hold in the original computer program. Furthermore, when an assertion is safe in the computer program and if after applying the loop abstraction process, the model checker returns the assertion to be safe then the original computer program is safe with respect to that assertion. [0018] These and other advantages of the present subject matter would be 20 described in greater detail in conjunction with the following figures. While aspects of described systems and methods for loop abstraction in a program can be implemented in different computing systems, environments, and/or configurations, the implementations are described in the context of the following exemplary system(s). [0019] Fig. 1 illustrates exemplary components of a loop abstraction system 25 102 implementing loop abstraction in a program written in a programming language, in accordance with an implementation of the present subject matter. The loop abstraction system 102 may be implemented in a computing device 128. Examples of the computing device 128 include, but are not limited to, mainframe computers, 8 workstations, personal computers, desktop computers, minicomputers, servers, multiprocessor systems, laptops, a cellular communicating device, such as a personal digital assistant, a smart phone, and a mobile phone; and the like. The loop abstraction system 102, implemented using the computing device 128, includes one 5 or more processor(s) 104, IO interface(s) 106, and a memory 108 coupled to the processor 104. The processor 104 can be a single processing unit or a number of units. The processor 104 may be implemented as one or more microprocessors, microcomputers, microcontrollers, digital signal processors, central processing units, state machines, logic circuitries, and/or any devices that manipulate signals based on 10 operational instructions. Among other capabilities, the processor 104 is configured to fetch and execute computer-readable instructions and data stored in the memory 108. [0020] Functions of the various elements shown in the figures, including any functional blocks labeled as “processor(s)”, may be provided through the use of dedicated hardware as well as hardware capable of executing software in association 15 with appropriate software. When provided by a processor, the functions may be provided by a single dedicated processor, by a single shared processor, or by a plurality of individual processors, some of which may be shared. Moreover, explicit use of the term “processor” should not be construed to refer exclusively to hardware capable of executing software, and may implicitly include, without limitation, digital 20 signal processor (DSP) hardware, network processor, application specific integrated circuit (ASIC), field programmable gate array (FPGA), read only memory (ROM) for storing software, random access memory (RAM), and non volatile storage. Other hardware, conventional and/or customized, may also be included. [0021] The IO interfaces 106 may include a variety of software and hardware 25 interfaces, for example, interface for peripheral device(s), such as a keyboard, a mouse, an external memory, and a printer. Further, the IO interfaces 106 may enable the computing device to communicate with other computing devices, such as a personal computer, a laptop, and like. 9 [0022] The memory 108 may include any computer-readable medium known in the art including, for example, volatile memory, such as static random access memory (SRAM) and dynamic random access memory (DRAM), and/or non-volatile memory, such as read only memory (ROM), erasable programmable ROM, flash 5 memories, hard disks, optical disks, and magnetic tapes. The memory 108 also includes module(s) 110 and data 120. [0023] The module(s) 110 include routines, programs, objects, components, data structures, etc., which perform particular tasks or implement particular abstract data types. The module(s) 110 further include a context expansion module 112, a 10 loop abstraction module 114, a model checker module 116 and other module(s) 118. The other module(s) 118 may include programs or coded instructions that supplement applications and functions of the computing device. [0024] On the other hand, the data 120, amongst other things, serves as a repository for storing data processed, received, and generated by one or more of the 15 module(s) 110. The data 120 includes, for example, original loop data 122, abstraction data 124, and other data 126. The other data 126 includes data generated as a result of the execution of one or more modules in the other module(s) 118. [0025] In one implementation, the computing device is configured to abstract loops included in a source code also referred to as a program. For the purpose, the 20 program is initially received by the context expansion module 112. In one implementation, the context expansion module 112 may receive the program from a compilation module (not shown) internal to the computing device. In another implementation, the context expansion module 112 may receive the program from a compilation module (not shown) external to the computing device. 25 [0026] On receiving the program, the context expansion module 112 saves the program in the original loop data 122 and analyzes syntax of the program to identify an original loop for which the loop abstraction may be performed. The original loop 10 may include an original loop body and an original loop statement. The original loop statement may be defined as the statement in the program that is provided to initiate a loop. The original loop statement is also referred to as control statement. The original loop statement typically includes, among other things, a termination condition for the 5 original loop. For example, in a “for” loop, the first statement “(for i =0; i<10; i++)” defining the “for loop” may be referred to as the original loop statement. Further, the original loop body may be defined as a set of one or more statements involving loop variables that are executed during the loop execution. For instance, in the previous example of the program received by the computing device 102, the context expansion 10 module 112 may select the function call context for which the abstraction is to be carried out and can pass it to the loop abstraction module 114, which can abstract the original loop and pass the abstracted loop to the model checker 116. Further, the context expansion module 112 may also be responsible for the expansion of the context if the assertion cannot be verified using that context as discussed later. 15 [0027] In one implementation, the loop abstraction module 114 is configured to replace the original loop with the abstracted loop to generate an abstracted source code. In one implementation, the loop abstraction module 114 may generate an abstract computer program by abstracting the loops present in the given context. The loop abstraction module 114 may take as input the function for analysis, and may 20 obtain the function call context and output variables present in the original loop from the context expansion module 112. To generate the abstract loop, the loop abstraction module 114 can add a modified expression for accelerated assignment of each output variable in a subset of the output variables. The modified expression can be added before the loop body. The loop abstraction module 114 can further replace the control 25 statement in the original loop with a bounded control statement. The bounded control statement can include a small known upper bound computed based on the number of blocks or the number of pure output variables. Further, the loop abstraction module 114 can replace the original loop with the abstract loop to generate an abstract source 11 code for the model checking. Here, the accelerated assignment indicates replacing the output variable with an abstracted output variable that has a value corresponding to a an iteration greater than the iteration being tested. Further, based on the variable being non-recurrent, self recurrent and the like, the accelerated assignment may vary, 5 as discussed later. In other implementations, methods known in the art may also be used for accelerated assignment. [0028] For an example, an original loop is provided below which is transformed into an abstracted loop which is an over-approximation of the original loop. The exemplary loop abstraction process (LA) is explained as follows: 10 Case 1: Property to be verified is inside the loop --------------------------------------------- ----------------------------------------------- ------ while ( c ) if( c ) Loop_body //base_case with property assertion //first loop 15 iteration { for( i=0 ; i=0); 10 5. l = l0 +k1; 6. assume(l < max); 7. if (l==last ) 8. st = 0; 9. l++; 15 10. } 11. assume(!(l < max)); Example B – An abstract loop (iloop_absbody) 1. j=0,p=0,l=0,st=0; 20 2. last=nondet(); max=nondet(); /* Base Case */ 3. st = 1; 4. if(st == 0 && l == last +1) 25 5. { 6. j+=3; p+=3; 7. } 8. if (st ==1) { 22 9. j++; 10 p++; 11 } 12 else { 5 13 j+=2; 14 p+=2; 15 } 16 if (l == last && st == 0) 17 j = j+1; 10 18 assert(j==p && l == max) ; 19 /* kth iteration*/ 15 20 for (t1 =0, l0 = l, j0 = j, p0 = p; t1<1 ; t1++) { 21 k1 = nondet(); k = nondet(); k2 = nondet(); k3 = nondet(); k4 = nondet(); k5 = nondet(); j = j0 + k2 + 2*k3 + 3*k5 + k4 ; p = p0 + k2 + 2*k3 + 3*k5; 22 l = l0 + k1; 23 __CPROVER_assume( k>=1 && k1>=0 && k2 >= 0 && k3>=0 && k4 20 >=0 && k5 >=0 ); 24 __CPROVER_assume( k == k2+k3+k5 && k4 <= k); 25 st = 1; 26 // Abstraction of inner loop only recurrence 27 for(t=0;t<2 && l=0); 30 l = l0 +k1; 31 __CPROVER_assume(l < max); 23 32 if (l==last ) 33 st = 0; 34 l++; 35 } 5 36 __CPROVER_assume(!(l < max)); 37 // Inner loop abstraction ended 38 if(st == 0 && l == last +1) 39 { 40 j+=3; p+=3; 10 41 } 42 else if (st ==1) 43 { 44 j++; 45 p++; 15 46 } 47 else { 48 j+=2; 49 p+=2; 50 } 20 51 if (l == last && st == 0) 52 j = j+1; 53 __CPROVER_assume(j==p && l == max) ; 54 } 25 /*(k+1)th Loop iteration*/ 55. st = 1; 56. 24 57 if(st == 0 && l == last +1) 58 { 59 j+=3; p+=3; 60 } 5 61 else if (st ==1) 62 { 63 j++; 64 p++; 65 } 10 66 else { 67 j+=2; 68 p+=2; 69 } 70 if (l == last && st == 0) 15 71 j = j+1; 72 assert(j==p && l == max) ; Example C - The Abstracted Code [0038] The technique is explained for the example C code shown in Example 20 A. It shows the original C code with a nested loop and an assertion and the corresponding abstracted code. Since assert lies outside the inner for loop (lines 7 - 12 of Example A), it is abstracted using loop replacement as shown in Example B of the example. The loop is replaced by another loop with two iterations as it has two blocks. The inner loop has one IO variable l that is part of a recurrence equation l + +. 25 It is therefore accelerated using the non-deterministic equation l = l + k1, where k1 is assigned a non-deterministic value representing the number of iterations that the original loop has taken. Inner loop abstraction body is referred as < iloop_absbody > in the abstracted code Example C. 25 [0039] The property of interest, the assertion at line 26 of Example A, lies within the outer loop and hence induction is applied to the outer loop. Lines 3-20 of the code in Example C check whether the assert holds at the end of the base case for induction. The inductive step is encoded by lines 20-54, where it is assumed the loop 5 has executed k times. The outer loop has IO variables l, j and p, which are given accelerated values l = l0 + k1; j = j0+k2+2*k3+k4+3*k5 and p = p0+k2+2*k3+3*k5 respectively at the end of the kth iteration. k2, k3, k4 and k5 are the number of times the bodies of the ‘else if’ construct at line 42, ‘else’ at line 47, ‘if’ at line 51 and ‘if’ at line 38 are executed at the end of k iterations. j0 and p0 are the initial values of j 10 and p respectively. Line 53 encodes the assumption that the property holds at the end of k iterations. Lines 55 - 72 encode the (k + 1)th iteration including the assert. [0040] The abstracted code is successfully verified by a model checker, for example the model checker may be a bounded model checker in this case. In the abstracted code, the state space of the variables j and p is a super set of that in the 15 concrete code making it a sound over-approximation. The loop abstraction process uses all three transformations - abstraction, acceleration and induction, to verify this code. In comparison, none of the commercially available tools (available model checkers, commercially available static analysis tools) were able to verify the original code. 20 [0041] Although implementations for loop abstraction in a program have been described in language specific to structural features and/or methods, it is to be understood that the appended claims are not necessarily limited to the specific features or methods described. Rather, the specific features and methods are disclosed as exemplary implementations for loop abstraction. 25 26 I/we claim: 1. A system for loop abstraction (102) in a source code, for model checking of 5 the source code, the system comprising: a context expansion module (112) 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 10 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 number of blocks is indicative of a count of unconditionally executed statement sets in 15 which at least one output variable is computed; and a loop abstraction module (114) 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 20 output variable in a first subset of the output variables, wherein the modified expression is added before the loop body; and replace 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 25 variable; and replace the original loop with the abstract loop to generate an abstract source code for the model checking. 27 2. The system for loop abstraction (102) in a source code as claimed in claim 1, wherein the output variables includes input-output variables and pure output variables, wherein the input-output variables are indicative of variables read and modified in the original loop, and the pure output variables are indicative 5 of variables modified without being read in the original loop, and wherein the first subset of the output variables corresponds to the input-output variables and the second subset of the output variables corresponds to pure output variables. 10 3. The system for loop abstraction (102) in a source code as claimed in claim 2, wherein the upper bound in the bounded control statement is a deterministic bound value computed based on a number of unconditionally executed statement sets in which at least one output variable is computed and the number of pure output variables. 15 . 4. The system for loop abstraction (102) in a source code as claimed in claim 1, wherein the loop abstraction module (114) configured to determine that an assertion statement is placed inside the original loop; 20 and apply induction to generate the abstract loop. 5. The system for loop abstraction (102) in a source code as claimed in claim 1, wherein for the accelerated assignment of a non-recurrent output variable, the 25 loop abstraction module is further configured to formulate the value of the non-recurrent output variable as a function of an initial value of the nonrecurrent variable, a number of reset expression for the non-recurrent variable, and the reset values of the reset expressions. 28 6. The system for loop abstraction (102) in a source code as claimed in claim 1, wherein for the accelerated assignment of a self recurrent output variable, the loop abstraction module is further configured to formulate the value of the self recurrent output variable as a function of, among other parameters an initial 5 value of the self recurrent output variable, a number of computations modifying the self recurrent output variable, and a number of times of execution of the computations in the original loop. 7. The system for loop abstraction (102) in a source code as claimed in claim 1, 10 further comprising: a model checker module (116) coupled to the processor to generate an error message for the abstract loop, wherein the error message corresponds to an occurrence of an error while model checking the abstract loop; and the context expansion module (112) configured to regenerate the 15 abstract loop in an expanded context, wherein the expanded context comprises execution statements outside the original loop that cause the original loop to be executed. 8. A method, implemented by a computer, for abstracting a loop in a source 20 code, for model checking of the source code, the method comprising: receiving the source code for abstraction; determining 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 25 control statement; identifying output variables in the original loop and a number of blocks associated with the original loop, wherein the number of blocks is 29 indicative of a count of unconditionally executed statement sets in which at least one output variable is computed; generating an abstract loop corresponding to the original loop, wherein the generating the abstract loop comprises: 5 adding a modified expression for accelerated assignment for each output variable in a first subset of the output variables, wherein the modified expression is added before the loop body; and replacing the control statement with a bounded control statement, wherein the bounded control statement includes an upper 10 bound based on the number of blocks, and count of a second subset of the output variable; and replacing the original loop with the abstract loop for generating an abstract source code for the model checking. 15 9. The method as claimed in claim 8, wherein the output variables includes input-output variables and pure output variables, wherein the input-output variables are indicative of variables read and modified in the original loop, and the pure output variables are indicative of variables modified without being read in the original loop, and wherein the first subset of the output 20 variables corresponds to the input-output variables and the second subset of the output variable corresponds to the pure output variables. 10. The method as claimed in claim 9, wherein the upper bound in the bounded control statement is a deterministic bound value computed based on a number 25 of unconditionally executed statement sets in which at least one pure output variable is computed. 30 11. The method as claimed in claim 8, wherein the generating the abstract loop comprises determining that an assertion statement is placed inside the original loop; and 5 applying induction for generating the abstract loop. 12. The method as claimed in claim 8, wherein the accelerated assignment of a non-recurrent output variable comprises formulating the value of the nonrecurrent output variable as a function of an initial value of the non-recurrent 10 variable, and a number of reset expression for the non-recurrent variable, and the reset values of the reset expressions, wherein the non-recurrent output variable is a function of a constant. 13. The method as claimed in claim 8, wherein the accelerated assignment of a 15 self recurrent output variable comprises formulating the value of the self recurrent output variable as a function of, among other parameters, initial value of the self recurrent output variable, a number of computations modifying the self recurrent output variable, and a number of times of execution of the computations in the original loop, wherein the self recurrent 20 output variable is a function of a constant and the self recurrent output variable. 14. The method as claimed in claim 8 further comprising, receiving an error message for the abstract loop from a model checker, 25 wherein the error message corresponds to an occurrence of an error while model checking the abstract loop; and 31 regenerating the abstract loop in an expanded context, wherein the expanded context comprises execution statements outside the original loop that cause the original loop to be executed. 5 15. The method as claimed in claim 8, wherein the generating the abstract loop comprises generating the abstract loop for each nested loop in the original loop starting from an inner most nested loop. 16. A non-transitory computer-readable medium having embodied thereon a 10 computer program for executing a method, for abstracting a loop in a source code, for model checking of the source code, the method comprising: receiving the source code for abstraction; determining an original loop within the source code, wherein the original loop includes a control statement and a loop body, wherein the 15 original loop causes the loop body to be repeatedly executed based on the control statement; identifying 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 20 least one output variable is computed; generating an abstract loop corresponding to the original loop, wherein the generating the abstract loop comprises: adding a modified expression for accelerated assignment for each output variable in a first subset of the output variables, wherein 25 the modified expression is added before the loop body; and replacing the control statement with a bounded control statement, wherein the bounded control statement includes an upper 32 bound based on the number of blocks and count of a second subset of the output variables; and replacing the original loop with the abstract loop for generating an abstract source code for the model checking. 5 17. The non-transitory computer-readable medium, as claimed in claim 16, wherein the generating the abstract loop comprises: determining that an assertion statement is placed inside the original loop; and 10 applying induction for generating the abstract loop. 18. The non-transitory computer-readable medium, as claimed in claim 16, wherein the accelerated assignment of a non-recurrent output variable, wherein the non-recurrent output variable is a function of a constant, 15 comprises formulating the value of the non-recurrent output variable as a function of initial value of the non-recurrent variable, and number of reset expression for the non-recurrent variable, and the reset values of the reset expressions, while the non-recurrent variable is a function of constants. 20 19. The non-transitory computer-readable medium, as claimed in claim 16, wherein the accelerated assignment of a self recurrent output variable comprises formulating the value of the self recurrent output variable as a function of, among other parameters, initial value of the self recurrent output 25 variable, a number of computations modifying the self recurrent output variable, and a number of times of execution of the computations in the original loop, wherein the self recurrent output variable is a function of a constant and the self recurrent output variable. 33 20. The non-transitory computer-readable medium, as claimed in claim 16 further comprising, receiving an error message for the abstract loop from a model checker, 5 wherein the error message corresponds to an occurrence of an error while model checking the abstract loop; and regenerating the abstract loop in an expanded context, wherein the expanded context comprises execution statements outside the original loop that cause the original loop to be executed.