Polyspace Code Prover Server is a sound static analysis engine that proves the absence of overflow, divide-by-zero, out-of-bounds array access, and certain other run-time errors in C and C++ code. It performs interprocedural analysis of all possible control and data flows, including multi-threaded code, to identify each operation as always safe, always faulty, unreachable, or vulnerable. Polyspace Code Prover Server identifies code segments that are free of run-time errors, proven to fail, unreachable, or unproven.
Polyspace Code Prover Server can run on a server-class machine and can be integrated into build and continuous integration systems for automated verification using tools such as Jenkins®. The analysis results can be published to Polyspace Access for triage and resolution.
Support for industry standards is available through IEC Certification Kit (for IEC 61508 and ISO 26262) and DO Qualification Kit (for DO-178).
Automate Code Analysis with Polyspace Code Prover Server
Prove the Absence of Critical Run-Time Errors
Analyze all code paths against all possible inputs without code execution. Identify statements that will never experience a run time error, regardless of the run-time conditions and find others that require attention.
Automate and Integrate into DevOps
Supports modern software development practices by plugging into existing DevOps workflows and tools. Polyspace® works with popular continuous integration tools such as Jenkins and Bamboo®.
Run Static Code Analysis on Any Platform
Run Polyspace Code Prover Server on an automation server on premise or in the cloud. Use MathWorks reference architectures to deploy on platforms such as Docker, AWS® and Azure®.
Certification Support
Create artifacts needed to complete the certification process for industry standards. TÜV SÜD certified for the highest function safety levels of IEC 61508 and ISO 26262. Supports DO-178C qualification.
Prevent Unintended Software Behavior
Identify all code sections that cannot be reached via any execution path and errors in logic and program structure.
Analyze Global Variable Usage
Reduce time spent on debugging issues from read/write operations on global variables. Identify unprotected shared and unused variables.
Static Application Security Testing
Prove the absence of critical security vulnerabilities such as buffer overflows, memory access, and numerical overflows. Reduce the need for Fuzz testing by analyzing code under all code paths and input without code execution.
Impact Analysis
Formally track and verify the impact of a specified global or local variable on other variables or specific statements. Perform signal analysis to fulfill requirements from the CARB for OBD related software, prove freedom from interference in the context of ISO 26262, and analyze calibration parameters effect. In the context of software security, perform taint analysis and tracking sensitive data flow.
Product Resources:
Polyspace Product Family
Polyspace products make critical code safe and secure by testing and monitoring software quality throughout the development lifecycle.
Polyspace Access
Identify coding defects, review static analysis results, and monitor software quality metrics.
Polyspace Code Prover Server
Continuously and exhaustively verify critical C and C++ code statements into CI pipelines.
Polyspace Bug Finder
Check coding rules, security standards, and code metrics, and find bugs.
Polyspace Test
Develop, manage, and execute tests for C and C++ code in embedded systems.
Polyspace Bug Finder Server
Identify software defects and enforce coding rules in your CI pipelines.
Polyspace Client for Ada
Exhaustively verify critical Ada statements units using formal methods.
Polyspace Code Prover
Exhaustively verify the most critical C and C++ statements using formal methods.
Polyspace Server for Ada
Continuously and exhaustively verify critical Ada code statements into CI pipelines.
