Get Started with Polyspace Code Prover

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 ISO 26262 and IEC 61508) and DO Qualification Kit (for DO-178).

Tutorials

Desktop

• Run Polyspace Code Prover on Desktop
  Check C/C++ code exhaustively for run-time errors.
• Review Code Prover Results in Polyspace Platform User Interface
  Interpret Polyspace Code Prover results, fix code or justify results, manage results.

Server and Web Interface

• Quick Start Guide for Polyspace Server and Access Products
  See what you need to do for setting up Polyspace runs for a project, team or organization.
• Run Polyspace Code Prover on Server and Upload Results for Web-based Review
  Check code after submission for run-time errors and upload results for review in web interface.

Deployment

• Source Code Verification with Polyspace Code Prover
  

  See how static analysis by Polyspace Code Prover helps you verify C and C++ code.

• Polyspace Products and Software Development Workflows
  

  Learn about Polyspace products that can be used in a software development life cycle.

• Differences Between Polyspace Bug Finder and Polyspace Code Prover
  

  Find out how Bug Finder and Code Prover complement each other and determine when to deploy each product in your development workflow.