STATIC PROGRAM ANALYSIS
SEMATIC VS SYNTACTIC
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.
Testing is also called dynamic program analysis. However, it is a well-known fact (as well as proved theoretically) that one cannot test a program on all the possible inputs and environment conditions. Indeed, on industrial software a developer can test only a minimal part of the program.