Claims:1. A computer implemented method for data structure abstraction in a source code, for model checking of the source code, the method comprising:
receiving a source code for abstraction;
identifying one or more data structure accesses in the source code, the one or more data structure accesses comprising expressions for referencing elements of a data structure to access the data structure in the source code;
identifying one or more loops in the one or more data structure accesses, a loop of the one or more loops comprising control statement and a loop body, wherein the loop causes the loop body to be repeatedly executed based on the control statement;
identifying one or more loop-types in the one or more loops;
generating an abstracted code based at least on the one or more loop types, the abstracted code capable of abstracting the data structure, wherein abstracting the data structure comprises performing, for each loop of the one or more loops:
replacing the one or more data structure accesses by one of a corresponding representative element and a non-deterministic value in the loop body of said loop based on the elements of the data structure being accessed in a current iteration of said loop,
eliminating loop control statement of said loop operating on the elements of the data structure based on a loop type of said loop, and
adding a plurality of non-array assignments at a start of the loop body and after the loop body of the source code; and
providing the abstracted code for the model checking.

2. The method as claimed in claim 1, wherein a data structure access of the one of more data structure accesses comprises one of an array, an hash table, a graph, a tree, a class, a set, and a map.
3. The method as claimed in claim 1, wherein the one or more loop types comprises a complete loop and a partial loop, wherein the complete loop comprises a loop iterating over all of the elements of the data structure and the partial loop comprises a loop iterating over a subset of the elements of the data structure.
4. The method as claimed in claim 3, wherein eliminating the loop control statement of said loop comprises:
determining the loop type of said loop to be the complete loop; and
replacing the loop control statement with an if (true) statement.

5. The method as claimed in claim 3, wherein eliminating the loop control statement of said loop comprises:
determining the loop type of said loop to be the partial loop; and
replacing the loop control statement with an if(non-deterministic) statement.

6. The method as claimed in claim 1, further comprising determining a location of occurrence of the data structure access, the location being one of a Left Hand Side (LHS) and Right Hand Side (RHS) of a statement of the source code.
7. The method as claimed in claim 6, wherein on determination that the location of occurrence of the data structure access to be the RHS of the statement of the source code, the method further comprises:
determining the accessed element such that the accessed element is associated with an iteration different from a current iteration of said loop; and
replacing the one or more data structure accesses by a corresponding non-deterministic value.

8. The method as claimed in claim 6, wherein on determination that the location of occurrence of the data structure access to be the LHS of the statement of the source code, the method further comprises:
replacing the one or more data structure accesses by a corresponding representative element.

9. The method as claimed in claim 6, comprising prior to adding the plurality of non-array assignments at the start of the loop body and after the loop body of the source code:
identifying non-data structure variables in the loop body in the LHS of the statement; and
assigning corresponding non-deterministic values to the non-data structure variables.

10. A computer implemented system for reconciliation of records comprising:
at least one memory; and
at least one processor, the at least one memory coupled to the at least one processor wherein the at least one processor is capable of executing programmed instructions stored in the at least one memory to:
receive a source code for abstraction;
identify one or more data structure accesses in the source code, the one or more data structure accesses comprising expressions for referencing elements of the data structures to access the data structure in the source code;
identify one or more loops in the one or more data structure accesses, a loop of the one or more loops comprising control statement and a loop body, wherein the loop causes the loop body to be repeatedly executed based on the control statement;
identify one or more loop-types in the one or more loops;
generate an abstracted code based at least on the one or more loop types, the abstracted code capable of abstracting the data structure, wherein abstracting the data structure comprises performing, for each loop of the one or more loops:
replace the one or more data structure accesses by one of a corresponding representative element and a non-deterministic value in the loop body of said loop based on the elements of the data structure being accessed in a current iteration of said loop,
eliminate loop control statement of said loop operating on the elements of the data structure based on a loop type of said loop, and
add a plurality of non-array assignments at a start of the loop body and after the loop body of the source code; and
provide the abstracted code for the model checking.

11. The system as claimed in claim 10, wherein a data structure access of the one of more data structure accesses comprises one of an array, an hash table, a graph, a tree, a class, a set, and a map.
12. The system as claimed in claim 10, wherein the one or more loop types comprises a complete loops and partial loop, and wherein a complete loop comprises a loop iterating over all of elements of the data structure and a partial loop comprises a loop iterating over a subset of elements of the data structure.
13. The system as claimed in claim 12, wherein to eliminate the loop control statement of said loop, the at least one processor is capable of executing programmed instructions to:
determine the loop type of said loop to be the complete loop; and
replace the loop control statement with an if (true) statement.

14. The system as claimed in claim 13, wherein to eliminate the loop control statement of said loop, the at least one processor is capable of executing programmed instructions to:
determine the loop type of said loop to be the partial loop; and
replace the loop control statement with an if(non-deterministic) statement.

15. The system as claimed in claim 10, wherein the at least one processor is capable of executing programmed instructions to determine a location of occurrence of the data structure access, the location being one of a Left Hand Side (LHS) and Right Hand Side (RHS) of a statement of the source code.
16. The system as claimed in claim 15, wherein on determination that the location of occurrence of the data structure access to be the RHS of the statement of the source code, the at least one processor is capable of executing programmed instructions to:
determine the accessed element such that the accessed element is associated with an iteration different from a current iteration of said loop; and
replace the one or more data structure accesses by a corresponding non-deterministic value.

17. The system as claimed in claim 15, wherein on determination that the location of occurrence of the data structure access to be the LHS of the statement of the source code, the at least one processor is capable of executing programmed instructions to:
replace the one or more data structure accesses by a corresponding representative element.

18. The system as claimed in claim 15, prior to adding the plurality of non-array assignments at the start of the loop body and after the loop body of the source code, the at least one processor is capable of executing programmed instructions to:
identify non-data structure variables in the loop body in the LHS of the statement; and
assign corresponding non-deterministic values to the non-data structure variables
, Description:As Attached