Polyspace
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
Automated static code analysis using formal methods for C/C++ and Ada
Quality
Find bugs and formally prove the absence of critical runtime errors - without test cases or code execution.
Safety
Meet safety standards and document compliance to MISRA, ISO 26262, IEC 61508, DO-178, and FDA regulations.
Security
Check software security vulnerabilities and standards such as CWE, CERT-C, ISO/IEC 17961, and others.
Nissan
Polyspace finds which operations can experience run-time errors, and also identifies those that will never have one, no matter the operating conditions.
Alenia Aermacchi
Polyspace static analysis tools check the code for run-time errors, ensure compliance with MISRA coding standards, and create artifacts for DO-178 certification credit.
Miracor
Polyspace helps Miracor demonstrate quality and correctness to the regulatory community, including the FDA, to prove that our device is safe.