Polyspace Code Prover
R2026bPolyspace® Code Prover™ analyzes all code paths against all possible inputs to prove the absence of certain run-time errors such as overflow, divide by zero, and out-of-bounds array access in C/C++ code. It also provides control and data flow insights, and proves the correctness of concurrent access of global variables shared across tasks (threads).
Polyspace Code Prover uses static analysis through abstract interpretation based on formal methods, producing results without requiring program execution, code instrumentation, or test cases. Results are easy to understand and actionable: they appear inline in the source code with color-coded findings, variable range information, and code navigation. You can use Polyspace Code Prover on any combination of C/C++ code, manually written or generated from Simulink® or an AI assistant.
Support for industry standards is available through IEC Certification Kit (for ISO 26262 and IEC 61508) and DO Qualification Kit (for DO-178).
Get Started
Learn the basics of Polyspace Code Prover
Installation
Install Polyspace products for analysis on desktop or server
Running Code Prover
Check C/C++ code for run-time errors in Polyspace Platform user interface, using scripts, or from other environments
Configuration
Emulate build, specify analysis constraints, and provide additional information necessary for optimal results from Code Prover
Continuous Integration
Run Code Prover Server for automated code checking on CI servers
Reviewing and Reporting Results
Investigate run-time errors (RTEs) found with Code Prover, fix or justify results, manage results review, and generate reports
Tool Qualification and Certification
Qualify Polyspace Code Prover for DO and IEC Certification
Troubleshooting in Polyspace Code Prover
Resolve unexpected issues in Polyspace Code Prover
