Overview of Polyspace Verification

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

To verify the source code, you set up verification parameters in a project, run the verification, and review the results. A graphical user interface helps you to efficiently review verification results. The software assigns a color to operations in the source code as follows:

  • Green – Indicates that an operation is proven to not have certain kinds of error.

  • Red – Indicates that an operation is proven to have at least one error.

  • Gray – Indicates unreachable code.

  • Orange – Indicates that the operation can have an error along some execution paths.

The color-coding helps you to quickly identify errors and find the exact location of an error in the source code. After you fix errors, you can easily run the verification again.

Was this topic helpful?