Accelerating the pace of engineering and science

Polyspace Code Prover

Diab Compiler Support

Diab Compiler Support

Set up Polyspace verification easily for code compiled with Wind River Diab compiler

Multitasking Code Verification Setup

Multitasking Code Verification Setup

Specify cyclic tasks and nonpreemptable interrupts directly as verification options

Polyspace API in MATLAB

Polyspace API in MATLAB

Configure and run Polyspace using MATLAB objects

Subnormal Float Detection

Subnormal Float Detection

Identify loss of precision from operations that lead to subnormal results

Improved Embedded Coder Support

Improved Embedded Coder Support

View more precise results when generated code uses lookup tables or large data structures

Autocompletion for Review Comments

Autocompletion for Review Comments

Partially type previous comment to select complete comment

S-Function Analysis

S-Function Analysis

Launch analysis of S-Function code from Simulink

Persistent Filter States

Persistent Filter States

Apply filters once and view filtered results across multiple runs

Floating-Point Support

Floating-Point Support

Propagate ranges more precisely for long double variables and enable verification mode to incorporate infinities and NaNs

Additional MISRA C:2012 Support

Additional MISRA C:2012 Support

Detect violations of all MISRA C:2012 rules except rules 22.x

Improved Concurrency Detection

Improved Concurrency Detection

View more precise sharing and protection results based on dynamic information such as data flow in branching statements and protection on individual fields of a structure

Option to Suppress Non-initialization Checks

Option to Suppress Non-initialization Checks

Customize verification by suppressing non-initialization checks

Microsoft Visual C++ 2013 Support

Microsoft Visual C++ 2013 Support

Analyze code developed in Microsoft Visual C++ 2013

Latest Releases

R2016b (Version 9.6) - 14 Sep 2016

Version 9.6, part of Release 2016b, includes the following enhancements:

Verification Setup

  • Diab Compiler Support: Set up Polyspace verification easily for code compiled with Wind River Diab compiler
  • Multitasking Code Verification Setup: Specify cyclic tasks and nonpreemptable interrupts directly as verification options
  • Polyspace API in MATLAB: Configure and run Polyspace using MATLAB objects

Verification Results

  • Subnormal Float Detection: Identify loss of precision from operations that lead to subnormal results
  • Improved Embedded Coder Support: View more precise results when generated code uses lookup tables or large data structures

See the Release Notes for details.

R2016a (Version 9.5) - 3 Mar 2016

Version 9.5, part of Release 2016a, includes the following enhancements:

  • Autocompletion for Review Comments: Partially type previous comment to select complete comment
  • S-Function Analysis: Launch analysis of S-Function code from Simulink
  • Persistent Filter States: Apply filters once and view filtered results across multiple runs
  • Floating-Point Support: Propagate ranges more precisely for long double variables and enable verification mode to incorporate infinities and NaNs

See the Release Notes for details.

R2015b (Version 9.4) - 3 Sep 2015

Version 9.4, part of Release 2015b, includes the following enhancements:

  • Option to Suppress Non-initialization Checks: Customize verification by suppressing non-initialization checks
  • Improved Concurrency Detection: View more precise sharing and protection results based on dynamic information such as data flow in branching statements and protection on individual fields of a structure
  • Microsoft Visual C++ 2013 Support: Analyze code developed in Microsoft Visual C++ 2013
  • Additional MISRA C:2012 Support: Detect violations of all MISRA C:2012 rules except rules 22.x

See the Release Notes for details.

R2015a (Version 9.3) - 5 Mar 2015

Version 9.3, part of Release 2015a, includes the following enhancements:

  • Simplified workflow for project setup and results review with a unified user interface
  • Review of code complexity metrics and global variable usage in user interface
  • Context-sensitive help for code complexity metrics, MISRA-C:2012, and custom coding rules
  • Detection of stack pointer dereference outside scope
  • Review of latest results compared to the last run

See the Release Notes for details.

R2014b (Version 9.2) - 2 Oct 2014

Version 9.2, part of Release 2014b, includes the following enhancements:

  • Support for MISRA C:2012
  • Improved verification speed
  • Support for Mac OS
  • Improved verification precision for non-initialized variables
  • Support for C++11
  • Context-sensitive help for verification options and checks

See the Release Notes for details.