Polyspace Code Prover



Polyspace Code Prover

Prove the absence of run-time errors in software

Polyspace Code Prover™ is a sound static analysis tool that proves the absence of overflow, divide-by-zero, out-of-bounds array access, and 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 semantic analysis and abstract interpretation based on formal methods to verify software interprocedural, control, and data flow behavior. You can use it to verify handwritten code, generated code, or a combination of the two. Each code statement is color-coded to indicate whether it is free of run-time errors, proven to fail, unreachable, or unproven.

Polyspace Code Prover displays range information for variables and function return values, and can prove which variables exceed specified range limits. Code verification results can be used to track quality metrics and check conformance with your software quality objectives. Polyspace Code Prover can be used with the Eclipse™ IDE to verify code on your desktop

Support for industry standards is available through IEC Certification Kit (for IEC 61508 and ISO 26262) and DO Qualification Kit (for DO-178).

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.

Latest Features

Project Authorization Management

Create and enforce authorization policies for access to project


Check for run-time mismatch between AUTOSAR specifications and code implementation

Stack Size Computation

Determine maximum stack usage by a C program and individual functions

Configuration from Build System

Automatically generate Polyspace configuration modules from build system

Multitasking Code Verification Setup

Specify cyclic tasks and nonpreemptable interrupts directly as verification options

See release notes for details on any of these features and corresponding functions.

Polyspace Code Prover™는 증명을 위한 정적 분석 도구로서, C와 C++ 소스 코드에서 오버플로우, 0으로 나누기, 경계 밖 배열 접근, 기타 런타임 오류가 없는지 증명합니다. 프로그램 실행, 코드 수정 또는 테스트 케이스 없이 결과를 제공합니다. Polyspace Code Prover는 정적 분석에 기반을 둔 의미 분석 및 Abstract Interpretation을 사용하여 소프트웨어 절차, 제어 및 데이터 흐름 동작을 검증합니다. 직접 작성한 코드, 생성된 코드 또는 이 두 가지가 조합된 코드에서 Polyspace Code Prover를 사용할 수 있습니다. 각 연산은 런타임 오류가 있는지, 실패가 검증되었는지, 도달할 수 없는지 또는 증명되지 않았는지 여부를 나타내는 색상 코드가 지정됩니다.

Polyspace Code Prover는 변수 및 함수 반환 값에 대한 범위 정보를 표시할 수 있고 변수가 지정된 범위 한도를 초과하는 조건을 증명할 수도 있습니다. 결과를 대시보드에 게시하여 품질 메트릭을 추적하고 소프트웨어 품질 목표를 준수할 수 있도록 합니다. 자동화된 검증을 위해 Polyspace Code Prover를 빌드 시스템에 통합할 수 있습니다.

업계 표준에 대한 지원은 IEC Certification Kit(IEC 61508 및 ISO 26262의 경우)와 DO Qualification Kit (DO‑178의 경우)를 통해 이용 가능합니다. Ada 언어 지원도 제공됩니다.

Get a Free Trial

30 days of exploration at your fingertips.

Download now

Ready to Buy?

Get pricing information and explore related products.

Are You a Student?

Get MATLAB and Simulink student software.

Learn more