Polyspace Code Prover Server

Prove the absence of run-time errors in software

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 Code Prover 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).

Getting Started

Learn the basics of Polyspace Code Prover Server

Configure and Run Analysis on Server

Set up automated runs of Code Prover at the command line or in a continuous integration platform such as Jenkins

Tool Qualification and Certification

Qualify Polyspace Code Prover Server for DO and IEC Certification

Troubleshooting in Polyspace Code Prover Server

Resolve unexpected issues in running Polyspace Code Prover Server