Static Analysis with Polyspace Products

Polyspace products can help you perform static analysis, which enables you to detect and prove the absence of overflow, divide-by-zero, out-of-bounds array access, and other run-time errors in source code.

Using advanced formal methods such as abstract interpretation, Polyspace products provide a complete solution for static code analysis — from enforcing coding rules, identifying bugs, and measuring code quality, to verifying that your handwritten or automatically generated code is infallible under all possible run-time conditions.


  • Detecting errors by finding bugs in source code
  • Formally proving the absence of errors in source code
  • Preventing errors with MISRA® C/C++, MISRA-AC-AGC, JSF++, or custom naming standards
  • Tracking software quality code metrics against appropriate software quality thresholds
  • Understanding run-time behavior from detailed range information of variables, functions, and call trees by tracing the control and data flow
  • Satisfying verification objectives and gaining credits for standards such as DO-178B/C, ISO 26262, IEC 61508, IEC 62304, and EN50128
  • Independently verifying and measuring code from Simulink®, dSPACE® TargetLink®, or IBM® Rational® Rhapsody®