PolySpace Embedded Software Verification

PolySpace® products verify C, C++, and Ada code for embedded applications by detecting run-time errors before code is compiled and executed. This advanced verification technology uses formal methods not only to detect errors, but to prove mathematically that certain classes of run-time errors do not exist.

You can use these tools on hand-written code, or code generated automatically from Model-Based Design tools.  For automatically generated code, PolySpace Link products trace results back to models to help you correct design errors.

Detect run-time errors and prove code correctness before compile time

PolySpace® Client™ for C/C++
PolySpace® Server™ for C/C++
PolySpace® Client™ for Ada
PolySpace® Server™ for Ada

Trace PolySpace results to external models

PolySpace® Model Link™ SL (for Simulink®)
PolySpace® Model Link™ TL (for dSPACE® TargetLink®)
PolySpace® UML Link™ RH (for Telelogic® Rhapsody®)

PolySpace® Jumpstart Service

Customized training and consulting for a fast, smooth transition to working with PolySpace products

FREE PolySpace Technical Kit

GET PolySpace Trial Software

Technical Support Resources

Documentation, knowledge base, case tracking, downloads, user community, and more

Transition Details for Existing PolySpace Customers

News

The MathWorks Acquires PolySpace Technologies, Leading Developer of Embedded System Code Verification Tools