# Documentation

## How Polyspace Verification Works

Polyspace® software uses static verification to prove the absence of run-time errors. Static verification derives the dynamic properties of a program without actually executing it. This technique differs significantly from other techniques, such as run-time debugging, in that the verification it provides is not based on a given test case or set of test cases. The dynamic properties obtained in the Polyspace verification are true for all executions of the software.

### What is Static Verification

Static verification is a broad term, and is applicable to any tool which derives dynamic properties of a program without actually executing it. However, most static verification tools only verify the complexity of the software, in a search for constructs which may be potentially erroneous. Polyspace verification provides deep-level verification identifying most run-time errors and possible access conflicts on global shared data.

Polyspace verification works by approximating the software under verification, using representative approximations of software operations and data.

For example, consider the following code:

```for (i=0 ; i<1000 ; ++i) {    tab[i] = foo(i); }```

To check that the variable `i` does not overflow the range of `tab`, a traditional approach would be to enumerate each possible value of `i`. One thousand checks would be required.

Using the static verification approach, the variable `i` is modelled by its domain variation. For instance, the model of `i` is that it belongs to the [0..999] static interval. (Depending on the complexity of the data, convex polyhedrons, integer lattices and more elaborate models are also used for this purpose).

An approximation usually leads to information loss. For instance, the information that `i` is incremented by one every cycle in the loop is lost. However, the important fact is that this information is not required to ensure that a range error will not occur; it is only necessary to prove that the domain variation of `i` is smaller than the range of `tab`. Only one check is required to establish that — and hence the gain in efficiency compared to traditional approaches.

Static code verification has an exact solution. However, this exact solution is not practical, as it would require the enumeration of all possible test cases. As a result, approximation is required for a usable tool.

### Exhaustiveness

Nothing is lost in terms of exhaustiveness. The reason is that Polyspace verification works by performing upper approximations. In other words, the computed variation domain of a program variable is a superset of its actual variation domain. The direct consequence is that a runtime error (RTE) item to be checked cannot be missed by Polyspace verification.