Main Content

Polyspace Code Prover

Prove the absence of run-time errors in software

Polyspace® Code Prover™ is a sound static analysis tool that proves the absence of overflow, divide-by-zero, out-of-bounds array access, and other run-time errors in C and C++ source code. It produces results without requiring program execution, code instrumentation, or test cases. Polyspace Code Prover uses semantic analysis and abstract interpretation based on formal methods to verify software interprocedural, control, and data flow behavior. You can use it to verify handwritten code, generated code, or a combination of the two. Each code statement is color-coded to indicate whether it is free of run-time errors, proven to fail, unreachable, or unproven.

Polyspace Code Prover displays range information for variables and function return values, and can prove which variables exceed specified range limits. Code verification results can be used to track quality metrics and check conformance with your software quality objectives. Polyspace Code Prover can be used with the Eclipse™ IDE to verify code on your desktop.

Support for industry standards is available through IEC Certification Kit (for IEC 61508 and ISO 26262) and DO Qualification Kit (for DO-178).

Get Started

Learn the basics of Polyspace Code Prover

Install Polyspace

Install Polyspace products for analysis on desktop or server

Configure and Run Analysis

Set up Polyspace Code Prover analysis on desktop or server

Review Analysis Results

Review Polyspace Code Prover results in Polyspace desktop user interface or web browser

Polyspace Code Prover Examples

Sample scripts and templates to run Polyspace Code Prover from different environments, C/C++ code examples showing run-time errors

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