Skip to Main Content Skip to Search
Home |   Select Country  Choose Country  |  Contact Us  |  Cart Store 
Create Account | Log In
Products & Services Solutions Academia Support User Community Company

Polyspace Embedded Software Verification

Nissan

"Polyspace products for C/C++ can ensure a level of software reliability that is unmatched by any tools in the industry."

Read the story

Delphi Diesel Systems

"Using Polyspace as soon as source code is available helps us catch bugs much earlier and thus at a much lower cost."

Read the story

EADS

"The Polyspace solution is unique - it detects run-time errors without execution and has the advantage of being exhaustive."

Read the story

IRSN

"Polyspace belongs to a new generation of analysis tools. It represents a large step forward for the verification of safety-related software."

Read the story

Code Verification with Static Analysis

Polyspace® code verifiers detect and prove the absence of overflow, divide-by-zero, out-of-bounds array access, and other run-time errors in source code. Polyspace uses static analysis that is formal methods based (with abstract interpretation) to verify C/C++ or Ada. You can use it to perform static code analysis and code verification of embedded software that is handwritten or generated. Polyspace can also be used to check compliance to coding standards and to measure software quality.

Polyspace helps you:

  • Detect difficult to find run-time errors in C/C++ and Ada
  • Enforce MISRA C®, MISRA-C++ or JSF++ (Joint Strike Fighter Air Vehicle C++) coding standards
  • Track software quality metrics and ensure that your software quality objectives have been met
  • Formally prove the absence of specific run-time errors (by abstract interpretation)
  • Create artifacts for certification to DO-178B, IEC 61508, and ISO 26262
  • Verify  handwritten or generated code from MathWorks Real-Time Workshop Embedded Coder™ (Simulink®), dSPACE® TargetLink®, or IBM® Rational® Rhapsody®

Learn more about Polyspace products for C/C++:

Polyspace Client™ for C/C++
Polyspace Server™ for C/C++

Polyspace products for Ada:

Polyspace Client™ for Ada
Polyspace Server™ for Ada

Polyspace products for generated code:

Polyspace Model Link™ SL (for Simulink®)
Polyspace Model Link™ TL (for dSPACE TargetLink)
Polyspace UML Link™ RH (for IBM Rational Rhapsody)

Support for industry certification standards:

IEC Certification Kit (for IEC 61508)
DO Qualification Kit (for DO-178)

Get more information: