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).
Learn the basics of Polyspace Code Prover Server
Set up automated runs of Code Prover at the command line or in a continuous integration platform such as Jenkins
Qualify Polyspace Code Prover Server for DO and IEC Certification
Resolve unexpected issues in running Polyspace Code Prover Server