Polyspace Code Prover

Verifying C and C++ Embedded Software

Polyspace Code Prover performs code verification of C and C++ embedded software that must operate at the highest levels of quality and safety. It uses a formal methods technique called abstract interpretation to produce sound verification results. Polyspace Code Prover identifies where run-time errors may occur and code that is proven to be safe from run-time errors. You use Polyspace Code Prover as part of a high quality assurance process to exhaustively verify all inputs, paths, and variable values. Polyspace Code Prover uses color-coding to indicate the status of each element in the code. It integrates with Simulink® to offer traceability of code level run-time results back to the Simulink models.

With Polyspace Code Prover, you can:

  • Prove your code — verify that your code is free of run-time errors
  • Obtain results with no false negatives — all potential run-time errors are exhaustively identified
  • Gain confidence in the quality of your code — measure proven versus unproven code

You can access Polyspace Code Prover from the command line, graphical user interface, or via plugins to Visual Studio® and Eclipse. You use it to support all critical activities in a software development workflow, including:

  • Detecting run-time errors
  • Proving the absence of certain run-time errors
  • Determining variable ranges and ensuring that range limits are not violated
  • Ensuring that the appropriate software quality objectives are met
  • Tracing run-time errors to Simulink blocks or IBM® Rational® Rhapsody® models
  • Creating artifacts for certification

Polyspace Code Prover works with Polyspace Bug Finder to find defects and check compliance to coding standards. These products offer an end-to-end static analysis capability for early stage development use, spanning bug-finding, coding rules checking, and proof of run-time errors. This capability ensures the reliability of embedded software that must operate at the highest levels of quality and safety.

You can speed up and offload code verification to a computer cluster by submitting verification jobs with Parallel Computing Toolbox and the MATLAB Distributed Computing Server.

Next: Detecting Run-Time Errors

Try Polyspace Code Prover

Get trial software

Comprehensive Static Analysis Using Polyspace Products

View webinar

Learn to Find, Analyze, and Fix Run-Time Errors in Your Code

Explore how