Main Content

Why Polyspace Verification Uses Approximations

Polyspace® Code Prover™ uses static verification to prove the absence of run-time errors. Static verification derives the dynamic properties of a program without actually executing it. Static verification differs significantly from other techniques such as run-time debugging because the verification does not rely on a specific test case or set of test cases. The properties obtained from static verification are true for all executions of your program1 .

Static verification uses representative approximations of software operations and data. For instance, consider the following code:

for (i=0 ; i<1000 ; ++i)  {
    tab[i] = foo(i); 
}
To check that the variable i never overflows the range of tab, one approach can be to consider each possible value of i. This approach requires a thousand checks.

In static verification, the software models a variable by its domain. In this case, the software models that i belongs to the static interval, [0..999]. Depending on the complexity of the data, the software uses more elaborate models such as convex polyhedrons or integer lattices for this purpose.

An approximation, by definition, leads to information loss. For instance, the verification loses the information that i is incremented by one every cycle in the loop. However, even without this information, it is possible to ensure that the range of i is smaller than the range of tab. Only one check is required to establish this property. Therefore, static verification is more efficient compared to traditional approaches.

When performing approximations, the verification does not compromise with exhaustiveness. The reason is that the approximations performed are upper approximations or over-approximations. In other words, the computed domain of a variable is a superset of its actual domain.

1 The properties obtained from static verification hold true only if you execute your program under the same conditions that you specified through the analysis options. For instance, the default verification assumes that pointers obtained from external sources are non-null. Unless you specify the option Consider environment pointers as unsafe (-stubbed-pointers-are-unsafe), the verification results are obtained under this assumption. They might not hold true during program execution if the assumption is invalidated and a null pointer is obtained from an external source.