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
Formal Proof of Absence of Critical Run-Time Errors
Prove the absence of certain run-time errors such as integer overflow, divide by zero, and out-of-bounds array access in C/C++ code. Enable early verification without tests or instrumentation. Prevent undefined behavior that can compromise robustness, safety, and security in embedded environments.
Automate Formal Code Verification Workflows
Integrate formal verification into CI pipelines. Automatically derive analysis configurations from build commands, and reuse configurations to ensure consistent results across teams and projects. Scale analyses across large and multiple codebases. Gate CI pipelines using machine-readable results.
Run Formal Code Verification in Any Environment
Integrate with third-party CI platforms and DevOps toolchains such as Jenkins®, GitHub®, GitLab®, or Bamboo®. Deploy on premises or in cloud environments such as AWS® or Azure®, and support container-based execution using Docker containers.
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 files to trace data propagation, function calls, and variable ranges at each statement. Identify unreachable or redundant code and verify alignment with architectural design or ARXML specifications.
Analysis of Global Variables and Concurrent Access Patterns
Analyze global variable read and write, including pointer-based access. Identify unprotected shared data across tasks or threads, unintended coupling between execution contexts, and concurrency risks affecting safety and security early in embedded software development.
Formal Static Application Security Testing
Eliminate critical C/C++ security vulnerabilities by proving that memory safety and run-time failures cannot occur, including buffer overflows, invalid memory access, and numeric overflows. Trace inputs to failing operations to model attack paths, assess exploitability, and prioritize security risk reduction.
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.
Centralize and Review Results in Polyspace Access
Upload Polyspace Code Prover Server results to Polyspace Access to centralize software quality data for team-based review and collaboration, alongside results from Polyspace Bug Finder Server and Polyspace Test. Triage findings, monitor run-time error checks over time, and evaluate compliance with defined software quality objectives.
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.
