Static Testing and static code analyzers

Static Testing is also called verification. It is also called dry run testing. In this the software is not actually used. It mainly checks the sanity of the code, algorithm or the document. This type of testing can be used by the developer who wrote the code, in isolation. Code reviews, inspections and walkthroughs are also used.
Static Code Analysis is a method of detecting errors in program code based on the programmer's reviewing the code marked by the analyzer in those places where potential errors may occur.
The main advantage of static code analyzers use lies in the possibility of considerable cost saving of defects elimination in a program. The earlier an error is determined, the lower is the cost of its correction. Static analysis tools allow to detect a large number of errors at the construction stage.

Formal methods is the term applied to the analysis of software (and hardware) whose results are obtained purely through the use of rigorous mathematical methods.
Implementation techniques of formal static analysis include:
- Model checking.
- Data-flow analysis.
- Abstract interpretation models.
- Use of assertions in program code.