Polyspace Code Prover

 

Polyspace Code Prover

Prove the absence of run-time errors in software

Get Started:

Verify Code Using Formal Mathematics

Achieve high levels of quality and safety with no false negatives.

Prove the Absence of Critical Run-Time Errors

Identify C/C++ and Ada code operations that will never experience a run-time error, regardless of the run-time conditions.

Detecting run-time errors

Detect Errors That Elude Other Means of Testing

Analyze all code paths against all possible inputs without code execution.

Call hierarchy.

Create Certification Artifacts

Complete the certification process for projects based on industry standards.

DO Qualification Kit.

Understand and Improve Code

Reduce time spent on code reviews, debugging, and robustness testing.

Understand the Root Cause of Issues and Improve Design

Examine control and data flow through software and see range information associated with variables and operators.

Tooltip displaying the possible ranges for all run-time conditions.

Prevent Unintended Software Behavior

Find all code sections that cannot be reached via any execution path and errors in logic and program structure.

Find dead code.

Trace Code Verification Results to Simulink Models

Run verification on generated code and trace findings to the source model block in Simulink.

Tracing code verification results to the Simulink model.

Automate Code Verification with Polyspace Code Prover Server

Enable continuous integration by performing analysis on code changes early and often.

Automating the Code Verification Process

Use Polyspace Code Prover Server™ to run the Polyspace Code Prover static analysis engine on a server-class machine with build automation tools such as Jenkins and Bamboo.

Automating the code verification process.

Notify and Upload Results for Collaborative Review

Automatically assign defects to component owners, send email notifications, and upload results to Polyspace Code Prover Access so you can triage and resolve issues.

Send email notifications with Polyspace Code Prover results.

Collaborative Review with Polyspace Code Prover Access

Share verification results and quality metrics with the software development team.

Review Polyspace Code Prover Results So You Can Triage and Resolve Issues

Polyspace Code Prover Access™ provides a web browser interface to Polyspace code verification results and quality metrics stored in a central repository. Use navigation tools in your web browser to investigate code verification results, which are displayed along with the code.

Detecting run-time errors

Project Quality and Software Quality Objectives

Dashboards display information that you can use to monitor software quality, project status, the number of defects, code metrics, and software quality objectives.

Project overview dashboard.

Integrate with the Bug Tracking Tools You Already Use

Use the web browser interface to create and assign tickets in bug tracking tools such as Jira.

Create ticket.