Polyspace Code Prover
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:
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:
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.