Software developers and verification engineers are ultimately responsible for the quality of the software they produce. Although developers can use manual techniques to quantify the quality of the software, these techniques are not necessarily exhaustive. Automation tools offer more consistent and in some cases more powerful techniques for producing high-quality software, including an automation technique known as static code analysis.
Static code analysis, also known as source code analysis or static analysis, is a software verification activity for analyzing source code for quality and reliability. This analysis enables software developers and testers to identify and diagnose errors such as overflows, divide-by-zero, and illegally dereferenced pointers.
Metrics produced by static code analysis provide a means for measuring and improving software quality. In contrast to other verification techniques, static code analysis can be performed without executing the program, developing test cases, or compiling the software program.
This article, published in EE Times, provides an introduction to formal methods and an example of formal methods analysis with Polyspace code verifiers.