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).
Formal Proof of Absence of Critical Run-Time Errors
Prove the absence of specific run-time errors (integer overflow, divide-by-zero, and out-of-bounds array access) in C/C++ by analyzing all paths and inputs without executing code. Enable early verification without tests or instrumentation. Prevent undefined behavior that can compromise robustness, safety, and security in embedded environments.
Sound Formal Methods-Based Code Verification
Perform sound static analysis using abstract interpretation to reason over all execution paths and inputs without executing code. Determine run-time error status directly in the source via color-coded annotations. Identify proven-safe behavior, definite defects, and code needing assumptions or design refinement.
Control- and Data-Flow-Based Architectural Understanding
Compute detailed control and data flow across functions and modules to trace data propagation and variable ranges at each statement. Identify unreachable or redundant code, and verify alignment with design or ARXML specifications.
Analysis of Global Variables and Concurrent Access Patterns
Analyze global variable reads and writes, including pointer-based and shared task or thread access, to expose control and data flow leading to unsafe concurrency. Identify unprotected shared data, unintended coupling between execution contexts, and concurrency risks affecting safety and security early in embedded software development.
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.
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.
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.
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.
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 Copilot
AI assistant optimized for Polyspace.
Polyspace Test
Develop, manage, and execute tests for C and C++ code in embedded systems.
Polyspace as You Code
Identify coding standard violations and software vulnerabilities from your IDE.
Polyspace Bug Finder
Check coding rules, security standards, and code metrics, and find bugs.
Polyspace Code Prover Server
Continuously and exhaustively verify critical C and C++ code statements into CI pipelines.
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.
