Polyspace Products



Making Critical Code Safe and Secure

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.

Polyspace Code Prover

Formally prove the absence of critical run-time errors without executing code

Polyspace Bug Finder

Check coding rules, security standards, code metrics, and find bugs

Polyspace for Ada

Prove the absence of run-time errors in source code

MATLAB Desktop

Automated static code analysis using formal methods for C/C++ and Ada

Deploy to Production Systems


Find bugs and formally prove the absence of critical runtime errors - without test cases or code execution.

Deploy to Production Systems


Meet safety standards and document compliance to MISRA, ISO 26262, IEC 61508, DO-178, and FDA regulations.

Deploy to Production Systems


Check software security vulnerabilities and standards such as CWE, CERT-C, ISO/IEC 17961, and others.