VO 1

Soundness = no false negatives

(A false negative is a missed bug in the code by the program analysis, i.e., the analysis

did not emit a warning for an existing bug)

Completeness = no false positives

(A false positive is a warning emitted by the program analysis for code that is correct)

Precision = trying to minimize incompleteness

It is typically faster

It becomes slower

• Absence of null pointer dereferences

• Assertions at a program point

• Termination

• Absence of data races

• Information flow

Abstract domains = standard abstractions for building abstract interpreters

-> They abstract program data, basic operations, and control

Abstract program state = a map from program variables to elements in the

abstract domain

Abstract transformer = describes the effect of statement and expression

evaluation on an abstract state

To obtain an over-approximation

-> We iterate until we reach a fixed point, which is the over-approximation of the program

If the over-approximation is correct, then the program must be correct

• Array bound checks (that is, buffer overflow)

• Division by zero

• Pointer checks (that is, NULL pointer dereference)

• Arithmetic overflow

• User-provided assertions (for example, assert i < j)

To check if the analysis remains sound:

-> If the unrolling assertions/assumptions hold, the analysis is sound