Description from "Polyspace code verifiers detect and prove the absence of overflow, divide-by-zero, out-of-bounds array access and other run-time errors in source code. Polyspace uses static code analysis that is formal methods based (with abstract interpretation) to verify C/C++ or Ada. Polyspace can also be used to check compliance to coding standards, review code complexity metrics, and measure software quality. " to "Polyspace® static code analysis products use formal methods to prove the absence of critical run-time errors under all possible control flows and data flows. They include checkers for coding rules, security vulnerabilities, code metrics, and hundreds of additional classes of bugs."
