FORM 2
THE PATENTS ACT, 1970
(39 of 1970)
&
THE PATENT RULES, 2003
COMPLETE SPECIFICATION
(See Section 10 and Rule 13)
Title of invention:
SYSTEM AND METHOD FOR FACILITATING A MODEL CHECKER BASED ELIMINATION OF FALSE POSITIVES
Applicant
Tata Consultancy Services Limited A Company Incorporated in India under The Companies Act, 1956
Having address:
Nirmal Building, 9th Floor,
Nariman Point, Mumbai 400021,
Maharashtra. India
The following specification particularly describes the invention and the manner in which it is to be performed.

CROSS-REFERENCE TO RELATED APPLICATIONS AND PRIORITY
[001] The present application claims priority to Indian Provisional Patent
Application No. 1679/MUM/2013, filed on May 9, 2013. the entirety of which is hereby incorporated by reference.
TECHNICAL FIELD
[002] The present subject matter described herein, in general, relates to warnings
generated during static analysis of an application code, and more particularly to facilitate a model checker based elimination of false positives.
BACKGROUND
[003] Software verification using abstract interpretation is scalable but imprecise.
The software verification using abstract interpretation has been effective in proving the absence of runtime errors such as Division by Zero (ZD), Array Index Out of Bound (AIOB) and buffer overflow. It has successfully been used to verify very large software systems, but generates too many false warnings, commonly referred to as false positives. On the other hand, model checking is precise for property verification but it often faces the state explosion problem as programs include unbounded-loops, recursions, and complex data structures. Under these circumstances, the property verification may not succeed.
[004] The existing techniques combine these techniques of abstract interpretation and
model checking to improve precision i.e., to generate fewer warnings which, in turn, would reduce the cost of their manual review. Abstract interpretation, being light weight is used first and then generated warnings are processed by a model checker to eliminate false positives. This processing includes generation of an assertion corresponding to each warning and its verification using a model checker. If an assertion is successfully verified, its corresponding warning is a false positive and is eliminated. This process of False Positives Elimination (FPE) is very time consuming as each assertion needs to be verified by a model checker, and an average assertion verification time is considerable.

SUMMARY
[005] This summary is provided to introduce aspects related to systems and methods
for facilitating a model checker based elimination of false positives generated during static analysis of an application code and the aspects are further described below in the detailed description. This summary is not intended to identify essential features of the claimed subject matter nor is it intended for use in determining or limiting the scope of the claimed subject matter.
[006] In one implementation, a method for facilitating a model checker based
elimination of false positives generated during static analysis of an application code is disclosed. The method comprises analyzing the application code in order to generate a plurality of warnings and generating a plurality of assertions, wherein each assertion of the plurality of assertions corresponds to a warning of the plurality of warnings. The method further qomprises identifying a set of run-time dependent loops used in the application code and determining one or more loops on which one or more assertions of the plurality of assertions are dependent, wherein the one or more loops are determined in a portion of the application code, wherein the portion is specified by an input verification code context. The method further comprises denoting one or more assertions as non-verifiable assertions when at least one of the one or more loops on which the assertions are dependent is amongst the set of run-time dependent loops, and dividing the plurality of assertions into a first set of assertions and a second set of assertions based upon the denoting, wherein the first set of assertions are non-verifiable assertions and the second set of assertions are verifiable assertions. The method further comprises skipping verification of the first set of assertions through the model checker, and verifying the second set of assertions through the model checker thereby facilitating elimination of false positives present in the plurality of warnings, wherein the analyzing, the generating, the identifying, the determining, the denoting, the dividing, the skipping and the verifying are performed by a processor using programmed instructions stored in a memory.
[007] In one implementation, a method for facilitating a model checker based
elimination of false positives generated during static analysis of an application code is disclosed. The method comprises analyzing the application code in order to generate a

plurality of warnings and generating a plurality of assertions, wherein each assertion of the plurality of assertions corresponds to a warning of the plurality of warnings. The method further comprises identifying a set of equivalent assertions from the plurality of assertions based upon a set of parameters and computing one or more leader assertions and one or more follower assertions from the set of equivalent assertions based upon a set of conditions. The method further comprises grouping the leader assertion and the one or more follower assertions of the leader assertion in a group and verifying the leader assertion in each group through the model checker and skipping a verification of the one or more follower assertions in each group, thereby facilitating elimination of false positives present in the plurality of warnings, wherein the analyzing, the generating, the identifying and the computing, the grouping, and the verifying are performed by a processor using programmed instructions stored in a memory.
[008] In one implementation, a system for facilitating a model checker based
elimination of false positives generated during static analysis of an application code is disclosed. The system comprises a processor and a memory coupled to the processor for executing a plurality of modules present in the memory. The plurality of modules comprises an analyzing module, a generation module, an identification module, a determining module, a denoting module, a dividing module, a skipping module and a verifying module. The analyzing module is configured to analyze the application code in order to generate a plurality of warnings. Further, the generation module is configured to generate a plurality of assertions. wherein each assertion of the plurality of assertions corresponds to a warning of the plurality of warnings. The identification module is configured to identify a set of run-time dependent loops used in the application code. The determining module is configured to determine one or more loops on which one or more assertions of the plurality of assertions are dependent upon, wherein the one or more loops are determined in a portion of the application code, wherein the portion is specified by an input verification code context. Further, the denoting module is configured to denote one or more assertions as non-verifiable assertions when at least one of the one or more loops on which the assertions are dependent is amongst the set of run-time dependent loops. The dividing module is configured to divide the plurality of assertions into a first set of assertions and a second set of assertions based upon the denoting, wherein the first set of assertions are non-verifiable assertions and the second set of assertions are verifiable

assertions and the skipping module configured to skip verification of the first set of assertions through the model checker. The verifying module is further configured to verify the second set of assertions through the model checker thereby facilitating elimination of false positives present in the plurality of warnings.
[009] In one implementation, a system for facilitating a model checker based
elimination of false positives generated during static analysis of an application code is disclosed. The system comprises a processor and a memory coupled to the processor for executing a plurality of modules present in the memory. The plurality of modules comprises an analyzing module, a generation module, an identification module, a computing module, a grouping module and a verifying module. The analyzing module configured to analyze the application code in order to generate a plurality of warnings. Further, the generation module configured to generate a plurality of assertions, wherein each assertion of the plurality of assertions corresponds to a warning of the plurality of warnings. Further, the identification module configured to identify a set of equivalent assertions from the plurality of assertions based upon a set of parameters and the computing module configured to compute one or more leader assertions and one or more follower assertions from the set of equivalent assertions based upon a set of conditions. The grouping module is configured to group the leader assertion and the one or more follower assertions of the leader assertion in a group and the verifying module is configured to verify the leader assertion in each group through the model checker and skipping a verification of the one or more follower assertions in each group, thereby facilitating elimination of false positives present in the plurality of warnings.
[0010] In one implementation, a computer program product having embodied thereon
a computer program for facilitating a model checker based elimination of false positives generated during static analysis of an application code is disclosed. The computer program product comprises of a program code for analyzing the application code in order to generate a plurality of warnings. The computer program product further comprises of a program code for generating a plurality of assertions, wherein each assertion of the plurality of assertions corresponds to a warning of the plurality of warnings. The computer program product further comprises of a program code for identifying a set of run-time dependent loops used in the application code and determining one or more Joops on which one or more assertions of the plurality of assertions are dependent upon, wherein the one or more loops are determined in a

portion of the application code, wherein the portion is specified by an input verification code context. The computer program product further comprises of a program code for denoting one or more assertions as non-verifiable assertions when at least one of the one or more loops on which the assertions are dependent is amongst the set of run-time dependent loops. The computer program product further comprises of a program code for dividing the plurality of assertions into a first set of assertions and a second set of assertions based upon the denoting, wherein the first set of assertions are non-verifiable assertions and the second set of assertions are verifiable assertions. The computer program product further comprises of a program code for skipping verification of the first set of assertions through the model checker, and a program code for verifying the second set of assertions through the model checker thereby facilitating elimination of false positives present in the plurality of warnings.
[0011] In one implementation, a computer program product having embodied thereon
a computer program for facilitating a model checker based elimination of false positives generated during static analysis of an application code is disclosed. The computer program product comprises of a program code for analyzing the application code in order to generate a plurality of warnings. The computer program product further comprises of a program code for generating a plurality of assertions, wherein each assertion of the plurality of assertions corresponds to a warning of the plurality of warnings. The computer program product further comprises a program code for identifying a set of equivalent assertions from the plurality of assertions based upon a set of parameters and a program code for computing one or more leader assertions and one or more follower assertions from the set of equivalent assertions based upon a set of conditions. The computer program product further comprises a program code for grouping the leader assertion and the one or more follower assertions of the leader assertion in a group and a program code for verifying the leader assertion in each group through the model checker and skipping a verification of the one or more follower assertions in each group, thereby facilitating elimination of false positives present in the plurality of warnings.

BRIEF DESCRIPTION OP THE DRAWINGS
[0012] The detailed description is provided with reference to the accompanying
figures. In the figures, the left-most digit(s) of a reference number identifies the figure in which the reference number first appears. The same numbers are used throughout the drawings to refer like features and components.
[0013] Figure 1 illustrates a network implementation of a system for facilitating a
model checker based elimination of false positives generated during static analysis of an application code, in accordance with an embodiment of the present subject matter,
[0014] Figure 2 illustrates the system, in accordance with an embodiment of the
present subject matter.
[0015] Figure 3 illustrates a method for facilitating a model checker based elimination
of false positives generated during static analysis of the application code, in accordance with art exemplary embodiment of the present subject matter,
[0016] Figure 4 illustrates a method for facilitating a model checker based elimination
of false positives generated during static analysis of the application code, in accordance with an embodiment of the present subject matter.
[0017] Figure 5 illustrates a method for facilitating a model checker based elimination
of false positives generated during static analysis of the application code, in accordance with an alternate embodiment of the present subject matter.
DETAILED DESCRIPTION
[0018] Systems and methods for facilitating a model checker based elimination of
false positives generated during static analysis of an application code are described. Initially. an application code may be analyzed using static analysis to generate one or more warnings. Further, an assertion may be generated for each warning. The assertions are analyzed to identify a set of equivalent assertions from the assertions. One or more leader assertions may be computed from the set of equivalent assertions and one or more follower assertions may be computed from the set of equivalent assertions for each of the computed leader assertions

based on a certain set of conditions. The leader assertion and the follower assertions of the leader assertions may be grouped together in a single group. The leader assertions from each group may be further verified by skipping the verification of the follower assertions, thereby facilitating faster elimination of false positives present in the plurality of warnings.
[0019] The application code may also be analyzed to identify a set of run-time
dependent loops. Further, one or more loops on which one or more assertions are dependent upon may be determined. The assertions may be denoted as non-verifiable assertions when at least one of the one or more loops on which the assertions are dependent is amongst the set of run-time dependent loops. Further, the verification of the assertions denoted as non-verifiable assertions may be skipped, thereby facilitating faster elimination of false positives present in the plurality of warnings.
[0020] While aspects of described system and method for facilitating elimination of
false positives generated during static analysis of an application code may be implemented in any number of different computing systems, environments, and/or configurations, the embodiments are described in the context of the following exemplary system.
[0021] Referring now to Figure 1, a network implementation 100 of a system 102 for
facilitating elimination of false positives generated during static analysis of an application code is illustrated, in accordance with an embodiment of the present subject matter. In one embodiment, the system 102 provides for identifying a set of equivalent assertions from the plurality of assertions based upon a set of parameters. The system 102 further may compute one or more leader assertions and one or more follower assertions from the set of equivalent assertions. The system 102 further groups the leader assertion and the one or more follower assertions of the leader assertion in a group. The system 102 performs a verification of the leader assertion computed from each group and skipping the verification of the one or more follower assertions in each group thereby facilitating elimination of false positives present in the plurality of warnings. The system 102 may also provide for identification of a set of runtime dependent loops used in the application code. Further, one or more loops on which one or more assertions are dependent upon may be determined. The assertions may be denoted as n on -verifiable assertions when at least one of the one or more loops on which the assertions are dependent is amongst the set of run-time dependent loops. Further, the verification of the

assertions denoted as non-verifiable assertions may be skipped, thereby facilitating faster elimination of false positives present in the plurality of warnings.
[0022] Although the present subject matter is explained considering that the system
102 is implemented on a server, it may be understood that the system 102 may also be implemented in a variety of computing systems, such as a laptop computer, a desktop computer, a notebook, a workstation, a mainframe computer, a server, a network server, and the like. It will be understood that the system 102 may be accessed by multiple users through one or more user devices 104-1, 104-2... 104-N, collectively referred to as user 104 hereinafter, or applications residing on the user devices 104. Examples of the user devices 104 may include, but are not limited to, a portable computer, a personal digital assistant, a handheld device, and a workstation. The user devices 104 are communicatively coupled to the system 102 through a network 106.
[0023] In one implementation, the network 106 may be a wireless network, a wired
network or a combination thereof. The network 106 can be implemented as one of the different types of networks, such as intranet, local area network (LAN), wide area network (WAN), the internet, and the like. The network 106 may either be a dedicated network or a shared network. The shared network represents an association of the different types of networks that use a variety of protocols, for example, Hypertext Transfer Protocol (HTTP), Transmission Control Protocol/Internet Protocol (TCP/IP), Wireless Application Protocol (WAP), and the like, to communicate with one another. Further the network 106 may include a variety of network devices, including routers, bridges, servers, computing devices, storage devices, and the like.
[0024] Referring now to Figure 2, the system 102 is illustrated in accordance with an
embodiment of the present subject matter. In one embodiment, the system 102 may include at least one processor 202, an input/output (I/O) interface 204, and a memory 206. The at least one processor 202 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 operational instructions. Among other capabilities, the at least one processor 202 is configured to fetch and execute computer-readable instructions stored in the memory 206.

[0025] The I/O interface 204 may include a variety of software and hardware
interfaces, for example, a web interface, a graphical user interface, and the like. The I/O interface 204 may allow the system 102 to interact with a user directly or through the client devices 104. Further, the I/O interface 204 may enable the system 102 to communicate with other computing devices, such as web servers and external data servers (not shown). The I/O interface 204 can facilitate multiple communications within a wide variety of networks and protocol types, including wired networks, for example, LAN, cable, etc., and wireless networks, such as WLAN, cellular, or satellite. The I/O interface 204 may include one or more ports for connecting a number of devices to one another or to another server.
[0026] The memory 206 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 memories, hard disks, optical disks, and magnetic tapes. The memory 206 may include modules 208 and data 210.
[0027] The modules 208 include routines, programs, objects, components, data
structures, etc., which perform particular tasks or implement particular abstract data types. In one implementation, the modules 208 may include an analyzing module 212, a generation module 214, an identification module 216, a determining module 218, a denoting module 220, a dividing module 222, a skipping module 224, a grouping module 226, a computing module 228, a verifying module 230 and other modules 232. The other modules 232 may include programs or coded instructions that supplement applications and functions of the system 102.
[0028] The data 210, amongst other things, serves as a repository for storing data
processed, received, and generated by one or more of the modules 208. The data 210 may also include a system database 234, and other data 236. The other data 236 may include data generated as a result of the execution of one or more modules in the other modules 232.
[0029] In one implementation, at first, a user may use the client device 104 to access
the system 102 via the I/O interface 204. The user may register them using the I/O interface 204 in order to use the system 102. The working of the system 102 may be explained in detail in Figure 3. The system 102 may be used for facilitating a model checker based elimination of false positives generated during static analysis of an application code. The system 102 further

comprises of the analyzing module 212 may be configured to analyze the application code in order to generate a plurality of warnings. The system 102 further comprises of the generation module 214 may be configured to generate a plurality of assertions, wherein each assertion of the plurality of assertions corresponds to a warning of the plurality of warnings. The identification module 216 may be configured to identify a set of run-time dependent loops.
[0030] In an exemplary embodiment of the system 102, a bounded model checker
(CBMC) may be used for verification of the assertions in ANSI-C and C++ programs. The CBMC takes an entry function, and a property to be verified that may be expressed as an assertion. The entry function specified represents a verification code context at which the assertion may be verified and can be an entry point of the application code or any other function having the input assertion. If the assertion holds for all execution paths, CBMC reports verification success. If the assertion does not hold for all execution paths, the CBMC generates an error trace leading to the property violation. The verification is performed by unwinding one or more loops in the program, and it is necessary for all the loops to have a finite upper bound. For the set of run-time dependent loops, it takes a user provided bound (unwinding count) as an upper bound. The provided bound should be enough to capture program semantics, so that the verification of the property is sound and complete. Further, when the bound is not enough, it warns by producing an unwinding error trace.
[0031] In the absence of the unwinding count the CBMC keeps unrolling the loop and
eventually runs out of memory. When the unwinding count is not insufficient, it results into an unwinding assertion counterexample. The verification of the unwinding assertion does not contribute in eliminating a false positive and is needless. The application code may include a set of run-time dependent loops whose bound is determined only at the run-time. The set of run-time dependent loops may include an infinite loop such as while(l), for(; ; ;), a loop in which a bound variable in its terminating condition takes values from library system calls, or a loop whose terminating condition is run-time dependent like *ptr! ='\0' and the string(s) pointed by ptr gets its content during run-time through fgets(pir).
[0032] In one embodiment of the system 102, the identification module 216 may be
configured to identify the set of run-time dependent loops used in the application code. The identification module 216 may use loop termination analysis as explained in A. Tsitovich, N.

Sharygina. C. Wintersteiger, and D. Kroening, "Loop summarization and termination analysis," in Tools and Algorithms for the Construction and Analysis of Systems, ser. Lecture Notes in Computer Science, P. Abdulla and K. Leino. Eds. Springer or A. Bradley, Z. Manna, and H. Sipma, "Termination analysis of integer linear loops." in CONCUR 2005 Concurrency Theory, ser. Lecture Notes in Computer Science, M. Abadi and L. Alfaro, Eds. Springer Berlin Heidelberg, 2005, vol. 3653, pp. 488-502. Berlin Heidelberg, 2011. vol. 6605, pp. 81-95.
[0033] The determining module 218 may configured to determine one or more loops
on which one or more assertions of the plurality of assertions are dependent upon, wherein the one or more loops are determined in a portion of the application code, wherein the portion is specified by an input verification code context. The input verification code context may be provided by the user as an input at which the assertion may be verified by the model checker. The input verification code context may be at a function level or at an application level. Also, the input verification code context may initially start with the function level and may expand further to the callers of a function in which the assertion is present, wherein, the function may be any function called directly or indirectly from the entry function. The function directly or indirectly may call another function in which the assertion being verified may be present. The denoting module 220 may be configured to denote one or more assertions as non-verifiable assertions (NVAs) when at least one of the one or more loops on which the assertions are dependent upon is amongst the set of run-time dependent loops. For each assertion 'A' and an entry function fe, the loops in fe, on which 'A' is control or data dependent may be identified. Program dependence graph may be used for such determining. The set of loops determined may be termed as L. Jf (L ∩ LUB)≠Ǿ then 'A' is a NVA in the context off,, wherein LUB is the set of run-time dependent loops, also referred as unbounded loops.
[0034] The assertion may be control or data dependent on the loops. An assertion 'A'
may be control or data dependent on a loop / if' A' is control or data dependent on a statement belonging to /. Referring to the program code 1 below,
char *str, charArr[20];
31.void f2(){
32. inti = 0;

33.... 34.while(*str!=,:){
35. assert( i>=0 && i<20);
36. charArr[i] = *str;
37. i++; 38.}
39. assert( i>=0 && i<20); 40.charArr[i] = '\0';
}
Throughout the specification, An is used to denote the assertion at line n and V (An) to denote the verification of the assertion An In the program code I. A35 and A39 may be denoted as the NVAs. This is because, each of them is control and data dependent on the run-time dependent loop starting at line 34.
[0035] The dividing module 222 may be configured to divide the plurality of
assertions into a first set of assertions and a second set of assertions based upon the denoting, wherein the first set of assertions are non-verifiable assertions and the second set of assertions are verifiable assertions. Further, the skipping module 224 may be configured to skip verification of the first set of assertions. The verifying module 230 may be configured to verify the second set of assertions through the model checker thereby facilitating elimination of false positives present in the plurality of warnings.
[0036] In an alternate embodiment of the system 102, the identification module 216
may be configured to identify a set of equivalent assertions from the second set of assertions based upon a set of parameters. The set of parameters may comprise structural similarity of an expression of the assertions, and a same source of values of variables referred to by the assertions.

[0037] Generally, many of the warnings generated may be similar and hence, their
corresponding assertions may be equivalent. The program code 2 below depicts a code snippet.
11. denom =...;
12.if(...){
13. assert(denom != 0); rl = nl/denom;
14.}
15.
16. assert(denom != 0); r2 = n2/denom;
17.
18.if(...){
19. assert(denom != 0); r3 = n3/denom;
20.}
The program code 2 depicts three Zero Division (ZD) warnings and their corresponding assertions. These warnings are similar, because the denominator in each ZD warning is the same variable and is taking values from the same source. They together represent a class of false positives or an error. Hence, the added assertions also may be equivalent. Thus, two assertions may be equivalent if their assert expressions are structurally similar and the variables referred to by these assertions have the same source for their values.
Referring program code 2, the assertions A13 A16, and A19 are the equivalent assertions.
[0038] The structural similarity of expressions requires that the variables used, the
operators and an order of appearance of the variables in the expression be the same. For example, given two ZD assertions with their expressions as:
(a + b + c)! = 0 and (a + b + c)! = 0 are potentially equivalent,
(v+1)! = 0 and (1+v)! = 0 are not equivalent, since operands appear in different order, and

(vl + func())! = 0 and (vl + func())! = 0 are not equivalent since different calls to a function can return different values.
[0039] Further, the computing module 228 may be configured to compute one or more
leader assertions and one or more follower assertions from the set of equivalent assertions based upon a set of conditions. The set of conditions may comprise: a particular assertion is a leader assertion only if all paths reaching any other assertion also go through that particular assertion. Consequently, an assertion A from the set of equivalent assertion may be computed as the leader assertion, only if all paths reaching any other follower assertion(s) (FAs) also go through A. The computation of the leader assertion and follower assertions of the leader assertion from the set of equivalent assertions is such that there are minimum number of the leader assertions and maximum number of the follower assertions. Referring program code 2, A|6 is computed as the leader assertion from the set of the equivalent assertions in the program code 2. Other assertions in the program code 2 (At3 or Ajg), cannot be tagged as the leader assertion for the follower assertion A]6 since there exists a path reaching Aie but not going through the other assertions (A 13 or A19).
[0040] Further, the grouping module 226 may be configured to group the leader
assertion and the one or more follower assertions of the leader assertion in a group. When the leader assertion does not have the follower assertion, the leader assertion may be the only member of the group, i.e., in the group there may be only one leader assertion and any number of follower assertions, including zero.
[0041] The computing module 228 may be further configured to compute Must
Reaching Assertions (MRAs) to compute the leader assertion and the one or more follower assertions of each of the leader assertion from the set of equivalent assertions in forward flow of information computation, or computing of Must Live Assertions (MLAs) to compute the leader assertions and the one or more follower assertions of each of the leader assertion from the set of equivalent assertions in backward flow of information computation, or a combination thereof. In an alternate embodiment, when the group consists of only the leader assertion and no follower assertions, the computing module is further configured to compute Must Reaching Assertions (MRAs) to compute the leader assertion from the set of equivalent assertions in forward flow of information computation, or computing of Must Live Assertions

(MLAs) to compute the leader assertions from the set of equivalent assertions in backward flow of information computation, or a combination thereof.
[0042] For the computation of MR As, an assertion with expression e at a program
point P is a MRA at its succeeding program point P' if every path coming to P' passes through P and, no path segment between P and P' contains a /-value occurrence of any of the r-value(s) of e. This ensures that each execution path through P' also includes P. Referring the program code 2, A16 is a MRA at A19. However, A16 is not a MRA at A13 since A13 appears before A15. Also, A13 is not a MRA at other two assertions since there exists a path which does not go through A13 but reaches to them (A16 and A19).
[0043] Data flow formalization used for computation of MRAs is presented at a
procedure level using forward information flow. The data flow formalization used for computation of MRAs considers one run-time property at a time. For example. MRAs for grouping/partitioning of Zero Division (ZD) and Array Index Out of Bound (AIOB) assertions may be computed separately. The equations below are depicted for a node n in a control flow graph as described in F. E. Allen, "Control flow analysis," S1GPLAN Not., vol. 5, no. 7, pp. 1-19, Jul, 1970, where n denotes either an assignment statement or an expression controlling the flow.


killlnfo (X, n) =
{A€X] (usedVars(A) ∩modifiedVars(n)) ± 0}
usedVars(A) = r-values from assertion A
modifiedVars(n) = 1-values from program statement n
[0044] In the above formalization. lnn represents the MRAs flowing-in to n, i.e., at the
start of n, whereas Out„ represents the MRAs flowing-out (i.e. at the exit) of n.'In„ equation uses intersection because the flow information being computed is must information. The information flowing in at a point is computed using the information flowing out of its predecessors, as the flow information may be computed in the forward direction. MRAs information is generated only at program points having assertions while kill information is computed at each variable modification point. In„ equation indicates that MRAs are computed at the procedure level. This equation may need a change if the MRAs are to be computed at the application level. The change is required to incorporate the effect of calling contexts and function call points.
[0045] For the computation of MLAs, an assertion with expression e at a program
point P is a MLA at its preceding program point P' if every path coming out of P' also passes through P and, no path segment between P' and P contains a /-value occurrence of any of the r-value(s) of e. This ensures each execution path having P' on it, also includes. Referring the program code 2, A16 is a MLA at An- However. A16, is not a MLA at A19 since A19 does not precede A16. Also, A19 is not a MLA at the other two assertion points. (A16 and A13) since there exists a path which does not go through A19 but reaches them (A16 and An).
[0046] The data flow formalization used for computation of MLAs is similar to the
computation of MRAs with only change being in the direction of information flow, wherein the direction of the information flow is backward in case of the computation of MLAs. In order to account for this change, the ln„ and Outn equations are changed as under. In„ and Outn denote the MLAs being computed at the exit and start of a program point n respectively.


lnn = (Gen„ +(Outn - Killn (Outn)
[0047] Further, the MRAs at the exit of the program point n ((flowing out of n) are
denoted as MRAs(n), and the MLAs at start of the program point n (flowing in at n) are denoted as MLAs(n), Assertions A and A', with their assert expressions as e and e' respectively, fall in the same group if e and e' are structurally similar and one of the following hold:
1. A € {MRAs (A')}] MLAs (A')). In this case, A' will be a FA and A can be the leader assertion.
2. A' €{MRAs (A) U MLAs (A)). In this case, A will be a FA and A' can be the leader assertion.
[0048] An assertion A can be selected as the leader assertion for a particular group if
for every other assertion A' in the particular group, A € (MRAs (A') U MLAs (A')). If more than one assertion in the particular group qualifies to be the leader assertion, one of the leader assertions may be randomly selected as the leader assertion.
[0049] In another embodiment of the system 102, the usage of MRAs and MLAs to
compute the leader assertion may not group the equivalent assertions from the set of equivalent assertions that are not definitely reachable from one another. In this case, the set of parameters comprising a pattern of the application code may be used to group the equivalent expressions. Program code 3 below depicts a code snippet.
11. denom = ...;
12.if(...){
13. assert(denom != 0); rl =nl/denom;
14.} else {
15. assert(denom != 0); r3 = n3/denom;
16.}

[0050] In the program code 3, A13 and A]5 may not be grouped together in spite of
being equivalent, because there will not be a MRA or a MLA available at an assertion point from another assertion,
[0051] Program code 4 below depicts a code snippet.
intrColors[10],gColors[10];
11. void fl(intr. int g){
12. unsigned int i = 0, n. temp; 13.
Kn = ...:
15. assert(n>=0&&n<10);
16. rColors[n] = r;
17. assert(n>=0&&n<10);
18. gColors[n] = g; 19.

20. i =...;
21. assert(temp=i++, temp>=0 && temp=0 && temp<10 );
24. gColors[i++] = ...;
}
[0052] Referring to the program code 4, A21 and A23 may not be identified as the
leader assertion and the follower assertion even though the result of V (A21) follows that of V (A23). In this case, the computation of MLAs may be changed to group the equivalent assertions together. Again, referring to the program code 4. the MLAs at the exit of a program point n are denoted as Oui(n) and the MLAs at the start of n are denoted as In(n). In the program code 1, A21 € Out (A21) but A23 € In (k21) because A23 gets killed at A21. This kill of

A23 omits the association of A21 (follower assertion) with A23 (leader assertion). In this method, the kill computation is avoided resulting into A23 €In (k21). Further, the algorithm to identify the LA and its associated FAs is used to compute the leader assertion.
[0053] The system 102 further comprises the verifying module 230 configured to
verify the leader assertion in each group of equivalent assertions, skipping a verification of the one or more follower assertions in each group. The successful verification of the leader assertion in a particular group indicates that the warnings corresponding to the assertions in the particular group are the false positives thereby eliminating all the warnings from the same group. If the verification of the leader assertion fails then verification of the follower assertions in the particular group most likely fails, hence in this case, all the warnings from the group to which the leader assertion belongs, will remain as the warnings and none of them will be eliminated being a false positive. Essentially, the verification result of the follower assertions in the particular group follows the verification result of the leader assertion. If the leader assertion does not have the follower assertion, the leader assertion will be an only member of the particular group.
[0054] In another embodiment of the system 102, the identification module 216 may
be configured to identify a set of equivalent assertions from the plurality of assertions based upon a set of parameters. The set of parameters may comprise structural similarity of an expression of the assertions, and a same source of values of variables referred to by the assertions. In an alternate embodiment, the set of parameters may comprise a pattern of the application code.
[0055] Further, the computing module 228 may be configured to compute one or more
leader assertions and one or more follower assertions from the set of equivalent assertions based upon a set of conditions. The set of conditions may comprise: a particular assertion is a leader assertion only if all paths reaching any other assertion also go through that particular assertion. Further, the grouping module 226 may be configured to group the leader assertion and the one or more follower assertions of the leader assertion in a group. When the leader assertion does not have the follower assertion, the leader assertion may be the only member of the group, i.e., in the group there may be only one leader assertion and any number of follower assertions, including zero.

[0056] The computing module 228 may be further configured to compute Must
Reaching Assertions (MRAs) to compute the leader assertion and the one or more follower assertions of each of the leader assertion from the set of equivalent assertions in forward flow of information computation, or computing of Must Live Assertions (MLAs) to compute the leader assertions and the one or more follower assertions of each of the leader assertion from the set of equivalent assertions in backward flow of information computation, or a combination thereof. In an alternate embodiment, when the group of consists of only the leader assertion, the computing module 228 may be configured to compute Must Reaching Assertions (MRAs) to compute the leader assertion from the set of equivalent assertions in forward flow of information computation, or computing of Must Live Assertions (MLAs) to compute the leader assertion from the set of equivalent assertions in backward flow of information computation, or a combination thereof.
[0057] Further, the verifying module 230 may be configured to verify the leader
assertion in each group through the model checker, skipping a verification of the one or more follower assertions in each group, thereby facilitating elimination of false positives present in the plurality of warnings. The successful verification of the leader assertion in a particular group indicates that the warnings corresponding to the assertions in the particular group are the false positives thereby eliminating all the warnings from the same group.
[0058] In an alternate embodiment of the system 102. prior to execution of the
verifying module 230, the identification module 216 may be configured to identify the set of run-time dependent loops used in the application code. Further, the determining module 218 may be configured to determine one or more loops on which the leader assertion from each group of equivalent assertions are dependent upon, wherein the one or more loops are determined in a portion of the application code, wherein the portion is specified by an input verification code context. The denoting module 220 may be configured to denote the leader assertion as non-verifiable leader assertion when at least one of the one or more loops on which the assertions are dependent is amongst the set of run-time dependent loops. The denoting module 220 may be configured to denote the leader assertion as non-verifiable leader assertion by implementing the same method by which the one or more assertions are denoted as non-verifiable assertions. Further, the skipping module 224 may be configured to

skip verification of the non-verifiable leader assertion. The assertion may be control or data dependent on the loops.
[0059] Figure 3, in an exemplary embodiment of the system 102 illustrates a method
for facilitating the model checker based elimination of false positives generated during static analysis of an application code. The application code in the form of a source code to be analyzed by a static analyzer (the analyzing module 212) is fed into the static analyzer. An annotator (the generation module 214) is used to generate assertions corresponding to each warning generated. Further, an annotated code with the assertions is fed to an Equivalent/Non-Verifiable Assertions Identifier. The Equivalent/Non-Verifiable Assertions Identifier comprises of the grouping module 226, the computing module, the identification module 216, the determining module 218, and the denoting module 220. The first component of the Equivalent/Non-Verifiable Assertions Identifier implements the MRA and MLA formalizations in context and flow sensitive way at the function level to identify the input set of assertions based on their equivalence and compute the one or more leader assertions and the follower assertions of each of the one or more leader assertions. Further, it updates an analysis warnings report to reflect the association of LAs and their FAs. The output of the first component is fed to the second component. The second component implements a property specific, i.e. depending on the pattern of the application code, algorithm to group LAs computed by the first component. The second component also updates the warnings report for its computed LAs and their FAs. The third component receives the LAs computed by the second component and determines NVAs from the LAs. The warnings of the LAs denoted as NVAs and their FAs continue to be warnings and the LAs not denoted as NVAs are fed to the assertion verifier (verifying module 230).
[0060] The assertions verifier component comprises mainly of the model checker (for
example, CBMC) and. may include other tools implementing techniques such as code slicing, loops abstractions to scale the model checker. The actual false positives elimination is performed by the assertions verifier. The assertions verifier eliminates warnings (false positives) corresponding to a LA and its FAs when the LA is verified successfully. If the verification fails or times out. the warnings corresponding to the LA and its FAs are not eliminated. This component may allow False Positive elimination (FPE) in three different settings, FPE at a function level, FPE at an application level, and FPE using a code context

expansion (Cfpe). In Cfpe, the assertions verifier component communicates with the third component to check if the assertion being verified with an entry function is a NVA, and on finding the assertion as a NVA, its further verifications are skipped (skipping module 224).
[0061] The system 102 facilitates an efficient and faster elimination of false positives
as the verification of the non-verifiable assertions as well as the follower assertions of the leader assertions are skipped by the model checker.
[0062] Referring now to Figure 4. a method 400 for facilitating a model checker based
elimination of false positives generated during static analysis of an application code is shown, in accordance with an embodiment of the present subject matter. The method 400 may be described in the general context of computer executable instructions. Generally, computer executable instructions can include routines,, programs, objects, components, data structures, procedures, modules, functions, etc., that perform particular functions or implement particular abstract data types. The method 400 may also be practiced in a distributed computing environment where functions are performed by remote processing devices that are linked through a communications network. In a distributed computing environment, computer executable instructions may be located in both local and remote computer storage media, including memory storage devices.
[0063] The order in which the method 400 is described is not intended to be construed
as a limitation, and any number of the described method blocks can be combined in any order to implement the method 400 or alternate methods. Additionally, individual blocks may be deleted from the method 400 without departing from the spirit and scope of the subject matter described herein. Furthermore, the method can be implemented in any suitable hardware, software, firmware, or combination thereof. However, for ease of explanation, in the embodiments described below, the method 400 may be considered to be implemented in the above described system 102.
[0064] At block 402, a method for analyzing the application code in order to generate
a plurality of warnings is described. In one implementation, the application code is analyzed to generate warnings by the analyzing module 212,
[0065] At block 404, a method for generating a plurality of assertions, wherein each
assertion of the plurality of assertions corresponds to a warning of the plurality of warnings, is

described. In one implementation, the plurality of assertions may be generated by the generation module 214.
[0066] At block 406, a method for identifying a set of run-time dependent loops used
in the application code, is described. In one implementation, the set of run-time dependent loops may be identified by the identifying module 216.
[0067] At block 408, a method for determining one or more loops on which one or
more assertions of the plurality of assertions are dependent upon, wherein the one or more loops are determined in a portion of the application code, and wherein the portion is specified by an input verification code context, is described. In one implementation, the one or more loops may be determined by the determining module 218.
[0068] At block 410, a method for denoting one or more assertions as non-verifiable
assertions when at least one of the one or more loops on which the assertions are dependent is amongst the set of run-time dependent loops, is described. In one implementation, the one or more assertions may be denoted by the denoting module 220.
[0069] At block 412, a method for dividing the plurality of assertions into a first set of
assertions and a second set of assertions based upon the denoting, wherein the first set of assertions are non-verifiable assertions and the second set of assertions are verifiable assertions, is described. In one implementation, the plurality of assertions may be divided by trie dividing module 222.
[0070] At block 414, a method for skipping verification of the first set of assertions, is
described. In one implementation, the verification of the first set of assertions is skipped by the skipping module 224.
[0071] At block 416, a method for verifying the second set of assertions through the
model checker thereby facilitating elimination of false positives present in the plurality of warnings, is described. In one implementation, the second set of assertions is verified by the verifying module 230,
[0072] Referring now to Figure 5, a method 500 for facilitating a model checker
based elimination of false positives generated during static analysis of an application code is shown, in accordance with an alternate embodiment of the present subject matter. The method

500 may be described in the general context of computer executable instructions. Generally, computer executable instructions can include routines, programs, objects, components, data structures, procedures, modules, functions, etc., that perform particular functions or implement particular abstract data types. The method 500 may also be practiced in a distributed computing environment where functions are performed by remote processing devices.that are linked through a communications network. In a distributed computing environment, computer executable instructions may be located in both local and remote computer storage media, including memory storage devices.
[0073] The order in which the method 500 is described is not intended to be construed
as a limitation, and any number of the described method blocks can be combined in any order to implement the method 500 or alternate methods. Additionally, individual blocks may be deleted from the method 500 without departing from the spirit and scope of the subject matter described herein. Furthermore, the method can be implemented in any suitable hardware, software, firmware, or combination thereof. However, for ease of explanation, in the embodiments described below, the method 500 may be considered to be implemented in the above described system 102.
[0074] At block 502, a method for analyzing the application code in order to generate
a plurality of warnings is described. In one implementation, the application code is analyzed to generate warnings by the analyzing module'212.
[0075] At block 504, a method for generating a plurality of assertions, wherein each
assertion of the plurality of assertions corresponds to a warning of the plurality of warnings, is described. In one implementation, the plurality of assertions may be generated by the generation module 214.
[0076] At block 506, a method for identifying a set of equivalent assertions from the
plurality of assertions based upon a set of parameters, is described. In one implementation, the set of equivalent assertions may be identified by the identification module 216.
[0077] At block 508, a method for computing one or more leader assertions and one or
more follower assertions from the set of equivalent assertions based upon a set of conditions. is described. In one implementation, the leader and follower assertions may be computed by the computing module 228.

[0078] At block 510. a method for grouping the leader assertion and the one or more
follower assertions of the leader assertion in a group, is described. In one implementation, the leader assertion and the one or more follower assertions may be grouped by the grouping module 226.
[0079] At block 512, a method for verifying the leader assertion in each group through
the model checker, and skipping a verification of the one or more follower assertions in each group, thereby facilitating elimination of false positives present in the plurality of warnings, is described. In one implementation, the leader assertion may be verified by the verifying module 230.
[0080] Although implementations for methods and systems for facilitating a model
checker based elimination of false positives generated during static analysis of an application code 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 examples of implementations for facilitating the model checker based elimination of false positives generated during static analysis of an application code.

WE CLAIM:
1. A method for facilitating a model checker based elimination of false positives generated during static analysis of an application code, the method comprising:
analyzing the application code in order to generate a plurality of warnings;
generating a plurality of assertions, wherein each assertion of the plurality of assertions corresponds to a warning of the plurality of warnings;
identifying a set of run-time dependent loops used in the application code;
determining one or more loops on which one or more assertions of the plurality of assertions are dependent upon, wherein the one or more loops are determined in a portion of the application code, and wherein the portion is specified by an input verification code context;
denoting one or more assertions as non-verifiable assertions when at least one of the one or more loops on which the assertions are dependent, is amongst the set of run-time dependent loops;
dividing the plurality of assertions into a. first set of assertions and a second set of assertions based upon the denoting, wherein the first set of assertions are non-verifiable assertions and the second set of assertions are verifiable assertions;
skipping verification of the first set of assertions through the model checker; and
verifying the second set of assertions through the model checker thereby facilitating elimination of false positives present in the plurality of warnings;
wherein the analyzing, the generating, the identifying, the determining, the denoting, the dividing, the skipping and the verifying are performed by a processor using programmed instructions stored in a memory.

2. The method of claim 1, further comprising:
identifying a set of equivalent assertions from the second set of the assertions based upon a set of parameters;
computing one or more leader assertions and one or more follower assertions from the set of equivalent assertions based upon a set of conditions;
grouping the leader assertion and the one or more follower assertions of the leader assertion in a group;
verifying the leader assertion in each group, skipping a verification of the one or more follower assertions in each group.
3. The method of claim 2, wherein the set of parameters comprises structural similarity of expressions of the assertions, and a same source of values for variables referred to by the assertions.
4. The method of claim 2, wherein the set of parameters comprises a pattern of the application code.
5. The method of claim 2, further comprising computing of Must Reaching Assertions (MRAs) to compute the leader assertion and the one or more follower assertions of each of the leader assertion from the set of equivalent assertions in forward flow of information computation, or computing of Must Live Assertions (MLAs) to compute the leader assertions and the one or more follower assertions of each of the leader assertion from the set of equivalent assertions in backward flow of information computation, or a combination thereof.
6. The method of claim 2, further comprising computing of Must Reaching Assertions (MRAs) to compute the leader assertion from the set of equivalent assertions in forward flow of information computation, or computing of Must Live Assertions (MLAs) to compute the leader assertions from the set of equivalent assertions in backward flow of information computation, or a combination thereof.

7. The method of claim 2, wherein the group consists of only one leader assertion and the one or more follower assertions of the leader assertion.
8. The method of claim 2, wherein successful verification of the leader assertion in a particular group indicates that the warnings corresponding to the assertions in the particular group are the false positives thereby eliminating all the warnings from the particular group.
9. The method of claim 1, wherein the assertion is control or data dependent on the loops.
10. A method for facilitating a model checker based elimination of false positives generated during static analysis of an application code, the method comprising:
analyzing the application code in order to generate a plurality of warnings;
generating a plurality of assertions, wherein each assertion of the plurality of assertions corresponds to a warning of the plurality of warnings;
identifying a set of equivalent assertions from the plurality of assertions based upon a set of parameters;
computing one or more leader assertions and one or more follower assertions from the set of equivalent assertions based upon a set of conditions;
grouping the leader assertion and the one or more follower assertions of the leader assertion in a group; and
verifying the leader assertion in each group through the model checker and skipping a verification of the one or more follower assertions in each group, thereby facilitating elimination of false positives present in the plurality of warnings;
wherein the analyzing, the generating, the identifying and the computing, the grouping, and the verifying are performed by a processor using programmed instructions stored in a memory,

11. The method of claim 10. further comprising, prior to verifying:
identifying a set of run-time dependent loops used in the application code;
determining one or more loops on which the leader assertion from each group of equivalent assertions are dependent upon, wherein the one or more loops are determined in a portion of the application code, wherein the portion is specified by an input verification code context;
denoting the leader assertion as non-verifiable leader assertion when at least one of the one or more loops on which the assertions are dependent, is amongst the set of run-time dependent loops; and
skipping verification of the non-verifiable leader assertion.
12. The method of claim 10. wherein successful verification of the leader assertion in a particular group indicates that the warnings corresponding to the assertions in the particular group are the false positives thereby eliminating all the warnings from the particular group.
13. The method of claim 10, wherein the set of parameters comprises structural similarity of an expression of the assertions, and a same source of values for variables referred to by the assertions.
14. The method of claim 10, wherein the set of parameters comprises a pattern of the application code, and a combination thereof.
15. The method of claim 10, further comprising computing of Must Reaching Assertions (MRAs) to compute the leader assertion and the one or more follower assertions of each of the leader assertion from the set of equivalent assertions in forward flow of information computation, or computing of Must Live Assertions (MLAs) to compute the leader assertion and the one or more follower assertions of each of the leader assertion from the set of equivalent assertions in backward flow . of information computation, or a combination thereof.

16. The method of claim 10, further comprising computing of Must Reaching Assertions (MRAs) to compute the leader assertion from the set of equivalent assertions in forward flow of information computation, or computing of Must Live Assertions (MLAs) to compute the leader assertions from the set of equivalent assertions in backward flow of information computation, or a combination thereof.
17. The method of claim 11, wherein the assertion is control or data dependent on the loops.
18. A system for facilitating a model checker based elimination of false positives generated during static analysis of an application code, the system comprising:
a processor; and
a memory coupled to the processor, wherein the processor is capable of executing a plurality of modules stored in the memory, and wherein the plurality of modules comprising:
an analyzing module configured to analyze the application code in order to generate a plurality of warnings;
a generation module configured to generate a plurality of assertions, wherein each assertion of the plurality of assertions corresponds to a warning of the plurality of warnings;
an identification module configured to identify a set of run-time dependent loops used in the application code;
a determining module configured to determine one or more loops on which one or more assertions of the plurality of assertions are dependent upon, wherein the one or more loops are determined in a portion of the application code, wherein the portion is specified by an input verification code context;
a denoting module configured to denote one or more assertions as non-verifiable assertions when at least one of the one or more loops on which the assertions are dependent, is amongst the set of run-time dependent loops;
a dividing module configured to divide the plurality of assertions into a first set of assertions and a second set of assertions based upon the denoting,

wherein the first set of assertions are non-verifiable assertions and the second set of assertions are verifiable assertions;
a skipping module configured to skip verification of the first set of assertions through the model checker; and
a verifying module configured to verify the second set of assertions through the model checker thereby facilitating elimination of false positives present in the plurality of warnings.
19. The system of claim 18. further comprising:
an identification module configured to identify a set of equivalent assertions from the second set of the assertions based upon a set of parameters;
a computing module configured to compute one or more leader assertions and one or more follower assertions from the set of equivalent assertions based upon a set of conditions;
a grouping module configured to group the leader assertion and the one or more follower assertions of the leader assertion in a group; and
a verifying module configured to verify the leader assertion in each group, skipping a verification of the one or more follower assertions in each group.
20. The system of claim 19. wherein the set of parameters comprises structural similarity of an expression of the assertions, and a same source of values for variables referred to by the assertions.
21. The system of claim 19, wherein the set of parameters comprises, a pattern of the application code.
22. The system of claim 19. wherein the computing module is further configured to compute Must Reaching Assertions (MRAs) to compute the leader assertion and the one or more follower assertions of each of the leader assertion from the set of equivalent assertions in forward flow of information computation, or computing of

Must Live Assertions (MLAs) to compute the leader assertions and the one or more follower assertions of each of the leader assertion from the set of equivalent assertions in backward flow of information computation, or a combination thereof.
23. The system of claim 19, wherein the computing module is further configured to
compute Must Reaching Assertions (MRAs) to compute the leader assertion from the set of equivalent assertions in forward flow of information computation, or computing of Must Live Assertions (MLAs) to compute the leader assertions from the set of equivalent assertions in backward flow of information computation, or a combination thereof.
24. The system of claim 19, wherein the group consists of only one leader assertion and the one or more follower assertions of the leader assertion.
25. The system of claim 19, wherein successful verification of the leader assertion in a particular group indicates that the warnings corresponding to the assertions in the particular group are the false positives thereby eliminating all the warnings from the particular group.
26. The system of claim 18, wherein the assertion is control or data dependent on the loops.
27. A system for facilitating a model checker based elimination of false positives generated during static analysis of an application code, the system comprising:
a processor; and
a memory coupled to the processor, wherein the processor is capable of executing a plurality of modules stored in the memory, and wherein the plurality of modules comprising:
an analyzing module configured to analyze the application code in order to generate a plurality of warnings;

a generation module configured to generate a plurality of assertions, wherein each assertion of the plurality of assertions corresponds to a warning of the plurality of warnings;
an identification module configured to identify a set of equivalent assertions from the plurality of assertions based upon a set of parameters;
a computing module configured to compute one or more leader assertions and one or more follower assertions from the set of equivalent assertions based upon a set of conditions;
a grouping module configured to group the leader assertion and the one or more follower assertions of the leader assertion in a group; and
a verifying module configured to verify the leader assertion in each group through the model checker and skipping a verification of the one or more follower assertions in each group, thereby facilitating elimination of false positives present in the plurality of warnings.
28. The system of claim 27, further comprising, prior to execution of the verification
module:
an identification module configured to identify a set of run-time dependent loops used in the application code;
a determining module configured to determine one or more loops on which the leader assertion from each group of equivalent assertions are dependent upon, wherein the one or more loops are determined in a portion of the application code, wherein the portion is specified by an input verification code context;
a denoting module configured to denote the leader assertion as non-verifiable leader assertion when at least one of the one or more loops on which the assertions are dependent, is amongst the set of run-time dependent loops; and
a skipping module configured to skip verification of the non-verifiable leader assertion.
29. The system of claim 27, wherein successful verification of the leader assertion in a
particular group indicates that the warnings corresponding to the assertions in the

particular group are the false positives thereby eliminating all the warnings from the particular group.
30. The system of claim 27, wherein the set of parameters comprises structural similarity of an expression of the assertions, and a same source of values for variables referred to by the assertions.
31. The system of claim 27, wherein the set of parameters comprises a pattern of the application code, and a combination thereof.
32. The system of claim 27. wherein the computing module is further configured to compute Must Reaching Assertions (MRAs) to compute the leader assertion and the one or more follower assertions of each of the leader assertion from the set of equivalent assertions in forward flow of information computation, or computing of Must Live Assertions (MLAs) to compute the leader assertions and the one or more follower assertions of each of the leader assertion from the set of equivalent assertions in backward flow of information computation, or a combination thereof.

33. The system of claim 27, wherein the computing module is further configured to compute Must Reaching Assertions (MRAs) to compute the leader assertion from the set of equivalent assertions in forward flow of information computation, or computing of Must Live Assertions (MLAs) to compute the leader assertions from the set of equivalent assertions in backward flow of information computation, or a combination thereof.
34. The system of claim 28. wherein the assertion is control or data dependent on the loops.
35. A computer program product having embodied thereon a computer program for facilitating a model checker based elimination of false positives generated during static analysis of an application code, the computer program product comprising:

a program code for analyzing the application code in order to generate a plurality of warnings;
a program code for generating a plurality of assertions, wherein each assertion of the plurality of assertions corresponds to a warning of the plurality of warnings;
a program code for identifying a set of run-time dependent loops used in the application code:
a program code for determining one or more loops on which one or more assertions of the plurality of assertions are dependent upon, wherein the one or more loops are determined in a portion of the application code, wherein the portion is specified by an input verification code context;
a program code for denoting one or more assertions as non-verifiable assertions when at least one of the one or more loops on which the assertions are dependent, is amongst the set of run-time dependent loops;
a program code for dividing the plurality of assertions into a first set of assertions and a second set of assertions based upon the denoting, wherein the first set of assertions are non-verifiable assertions and the second set of assertions are verifiable assertions;
a program code for skipping verification of the first set of assertions through the model checker; and
a program code for verifying the second set of assertions through the model checker thereby facilitating elimination of false positives present in the plurality of warnings.
36. A computer program product having embodied thereon a computer program for facilitating a model checker based elimination of false positives generated during static analysis of an application code, the computer program product comprising:
a program code for analyzing the application code in order to generate a plurality of warnings;

a program code for generating a plurality of assertions, wherein each assertion of the plurality of assertions corresponds to a warning of the plurality of warnings:
a program code for identifying a set of equivalent assertions from the plurality of assertions based upon a set of parameters;
a program code for computing one or more leader assertions and one or more follower assertions from the set of equivalent assertions based upon a set of conditions;
a program code for grouping the leader assertion and the one or more follower assertions of the leader assertion in a group; and
a program code for verifying the leader assertion in each group through the model checker and skipping a verification of the one or more follower assertions in each group, thereby facilitating elimination of false positives present in the plurality of warnings.