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.