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 Polyspace Code Prover Analysis Results
  Interpret Polyspace Code Prover results, fix code or justify results, manage results.

Polyspace Platform User Interface

• Polyspace Platform: A Unified Platform for Static Analysis and Dynamic Testing
  Polyspace Platform is an integrated environment for static analysis and testing of C/C++ code with Polyspace products.
• Benefits and Limitations of Switching to Polyspace Platform User Interface
  Import projects created in older user interface, run tests or static analysis on imported projects.
• Run Polyspace Code Prover in Polyspace Platform User Interface
  Check C/C++ code exhaustively for run-time errors.
• Review Polyspace Code Prover Analysis 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 to Web Interface
  Check code after submission for run-time errors and upload results for review in web interface.
• Triage and Assign Results in Polyspace Access Web Interface (Polyspace Access)
  Navigate the dashboard, filter results, and assign issues to team members.
• Send Email Notifications with Polyspace Code Prover Server Results
  Send e-mails to developers with attachments containing links to Polyspace results.
• View Assigned Results in Polyspace Access Web Interface (Polyspace Access)
  See the results that are assigned to you.

Desktop to Server

• Send Code Prover Analysis from Desktop to Locally Hosted Server
  Offload Polyspace analysis to a locally hosted server and review downloaded results on desktop.

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.

• Workflow Using Both Polyspace Bug Finder and Polyspace Code Prover
  

  Incorporate Bug Finder and Code Prover analyses in your software development workflow.