Polyspace Code Prover

Prove the absence of run-time errors in software

Polyspace Code Prover proves the absence of overflow, divide-by-zero, out-of-bounds array access, and certain 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 static analysis and abstract interpretation based on formal methods. You can use it on handwritten code, generated code, or a combination of the two. Each operation is color-coded to indicate whether it is free of run-time errors, proven to fail, unreachable, or unproven.

Polyspace Code Prover also displays range information for variables and function return values, and can prove which variables exceed specified range limits. Results can be published to a dashboard to track quality metrics and ensure conformance with software quality objectives.

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

What Is Polyspace Code Prover?

Using code prover results and source code colors.

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.

Documentation

Display of tooltip with range possibilities for run-time conditions.

Improve Software Design and Code Understanding

Examine control and data flow through your C/C++ code and see range information associated with variables and operators.

Documentation

Detecting dead code in logic and program structure.

Optimize Software for Performance

Remove defensive code by identifying safe and secure operations such as division by zero and overflows. Detect code branches that cannot be reached via any execution path. Find errors in logic and program structure, remove them for smaller memory footprint.

Documentation

Analyze Global Variable Usage

Reduce time spent debugging read/write operations on global variables, including variables shared by tasks or threads.
Use the concurrent access graph to understand control and data flow that can lead to data race issues. Identify unused global variables for code optimization.

Documentation

Certification Support

Create artifacts needed to complete the certification process for industry standards. Certification completed by TÜV SÜD for use with IEC 61508 and ISO 26262 standards. Use reports and artifacts for DO-178C processes.

Documentation

Simulink and Stateflow Integration

Run analysis on generated code and trace your findings to source Simulink model blocks and Stateflow charts. Launch Polyspace^® analysis from within the Simulink environment.

Documentation

Interactive Analysis on Desktop

Run static code analysis on entire or subset of software projects. Use the desktop tool to generate reports, and review and triage results.
Find the root-cause of complex bugs with debugger-like views to navigate step-by-step through each statement leading to a run-time error. Organize and configure your projects, with native support of more than 60 C and C++ compilers, and automatic setup of Polyspace analysis extracted from the build system of the project.

Documentation

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.