Get Started with Polyspace Code Prover

Polyspace^® Code Prover™ analyzes all code paths against all possible inputs to prove the absence of certain run-time errors such as overflow, divide by zero, and out-of-bounds array access in C/C++ code. It also provides control and data flow insights, and proves the correctness of concurrent access of global variables shared across tasks (threads).

Polyspace Code Prover uses static analysis through abstract interpretation based on formal methods, producing results without requiring program execution, code instrumentation, or test cases. Results are easy to understand and actionable: they appear inline in the source code with color-coded findings, variable range information, and code navigation. You can use Polyspace Code Prover on any combination of C/C++ code, manually written or generated from Simulink^® or an AI assistant.

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 lifecycle.

• 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.