Program analysis aims at inferring and proving properties on software. Any developer tests his code after writing it, that is, it executes her software using some specific inputs and environment conditions. At the end of the test, the developer might
- have found a bug, or
- be sure that with those inputs and environment conditions the program behaves correctly.
A different approach was taken by static program analysis. This approach looks to the software without executing it. Compilers widely apply static analysis. For instance, the Java compiler discovers that a local variable might have not been initialized, or that a wrong value is assigned to a variable (e.g., if the program tries to assigns 1 to a String object). These errors are discovered statically without actually executing the code. An additional property of some static analyses is soundness. This guarantees that, if the static analyzer tells that a program satisfies a given property, then all the executions of the program will respect that property. For instance, a static analyzer might be able to prove that a program cannot raise a NullPointerException.