A processor implemented method for verification of a source code, comprising: receiving a source code encoded with one or more specifications to be verified, via one or more hardware processors; performing, via the one or more hardware processors, static analysis of the source code to identify one or more program features of the source code, the one or more program features comprising at least one of multiple return paths, loops with an unstructured control flow, loops with arrays, short ranges and numerical loops, wherein the static analysis is performed by carrying out one of an analysis of the one or more program features in a predefined sequential order and an analysis of the one or more program features in parallel; performing, via the one or more hardware processors, a structural analysis of loops and an interval analysis of input values read in loops to determine a predefined order of a plurality of verification techniques to verify the source code based on loops and a program control flow; and applying one or more verification techniques associated with the one or more program features to the source code for the verification, via the one or more hardware processors, wherein each verification technique of the one or more verification techniques is applied for a predetermined period of time and in a predefined order, wherein a verification technique from the plurality of verification techniques for verification of source code comprising loops with inputs of short ranges, comprises an explicit state model checking technique and loop invariant generation techniques and wherein the loop invariant generation techniques result in abstraction of the loop, wherein when the explicit state model checking technique cannot scale, two loop invariant generation techniques are applied simultaneously, wherein one of the loop invariant generation technique uses fuzz testing and program syntax analysis to guess and check candidate loop invariants, and another loop invariant generation technique is a counter-example guided loop abstraction refinement (CEGLAR) technique that havocs output variables of each loop and applies induction to each loop containing user properties to abstract the loop. receiving a source code encoded with one or more specifications to be verified, via one or more hardware processors; performing, via the one or more hardware processors, static analysis of the source code to identify one or more program features of the source code, the one or more program features comprising at least one of multiple return paths, loops with an unstructured control flow, loops with arrays, short ranges and numerical loops, wherein the static analysis is performed by carrying out one of an analysis of the one or more program features in a predefined sequential order and an analysis of the one or more program features in parallel; performing, via the one or more hardware processors, a structural analysis of loops and an interval analysis of input values read in loops to determine a predefined order of a plurality of verification techniques to verify the source code based on loops and a program control flow; and applying one or more verification techniques associated with the one or more program features to the source code for the verification, via the one or more hardware processors, wherein each verification technique of the one or more verification techniques is applied for a predetermined period of time and in a predefined order, wherein a verification technique from the plurality of verification techniques for verification of source code comprising loops with inputs of short ranges, comprises an explicit state model checking technique and loop invariant generation techniques and wherein the loop invariant generation techniques result in abstraction of the loop, wherein when the explicit state model checking technique cannot scale, two loop invariant generation techniques are applied simultaneously, wherein one of the loop invariant generation technique uses fuzz testing and program syntax analysis to guess and check candidate loop invariants, and another loop invariant generation technique is a counter-example guided loop abstraction refinement (CEGLAR) technique that havocs output variables of each loop and applies induction to each loop containing user properties to abstract the loop.