Polyspace
Polyspace 是靜態程式分析的工具，利用抽象釋義的方式進行大規模的分析，可以偵測 C 語言、C++ 或是 Ada 程式的原始碼中，是否有特定類型的執行期錯誤，或是證明沒有這類的錯誤。此工具也可以檢查原始碼是否符合特定的代碼標準（如 MISRA C/C++, SEI CERT C/C++ (CWE), JSF AV C++, AUTOSAR C++）。