验证编码规则并证明不存在运行时错误。这些特性保证了嵌入式软件的稳健性，使其能够在最高质量和安全性水平下运行。.
Polyspace Code Prover 是一款形式化方法验证工具，用于验证代码的正确性。负责代码安全和认证的工程师可以使用 Polyspace Code Prover 实时可靠地确定错误可能发生的位置。基于测试的彩色编码结果简化了验证任务，从而提高了软件开发效率和质量。Polyspace Code Prover 还利用 MATLAB 平台，为用户提供强大的 MATLAB 功能，例如跨团队集群的稳健作业分配、自动化脚本编写、结果可视化以及用于认证的报告生成。Polyspace Code Prover 集成了之前在 Polyspace Client for C/C++ 和 Polyspace Server for C/C++ 中提供的功能。.
Polyspace Bug Finder 可识别嵌入式软件中的运行时错误、数据流问题和其他缺陷。它通过静态分析，分析软件的控制行为、数据流和过程间交互行为，从而检测各种缺陷，例如数值错误、内存错误以及其他编程错误。与传统的人工审查不同，Polyspace Bug Finder 使工程师能够快速识别、筛选和纠正代码缺陷，从而加速开发流程。该工具还能检查代码是否符合 MISRA 和 JSF++ 等编码规则标准以及自定义规则，并生成代码质量和复杂度指标。与 Polyspace Code Prover 类似，Polyspace Bug Finder 也利用 MATLAB 平台将任务分发给团队集群、编写脚本并可视化结果。这两款产品都与 Simulink 集成，可用于处理自动生成的代码。.
MathWorks 设计自动化市场总监 Paul Barnard 表示：“Polyspace 产品系列提供全面的代码验证解决方案，让工程师在整个开发过程中对嵌入式软件的质量和安全性更有信心。Polyspace Bug Finder 和 Polyspace Code Prover 结合了静态分析和代码验证技术，采用形式化方法，帮助工程师在设计过程早期发现缺陷，并证明其软件安全可靠，可以部署。”
Polyspace 代码验证器和 Polyspace 错误查找器现已推出。.
