Polyspace Code Prover 会针对所有可能的输入对所有代码路径进行分析，以证明 C/C++ 代码中不存在某些运行时错误，例如溢出、除以零以及数组越界访问。它还提供控制流和数据流方面的深入洞见，并证明跨任务（线程）共享的全局变量的并发访问是正确的。
Polyspace Code Prover 通过基于形式化方法的抽象解释来使用静态分析，无需执行程序、代码插桩或测试用例即可产生结果。结果易于理解且可操作：它们以颜色编码的调查结果、变量范围信息以及代码导航的形式内联显示在源代码中。您可以将 Polyspace Code Prover 用于任何组合的 C/C++ 代码，无论是手动编写的还是由 Simulink 或 AI 助手生成的。
通过 IEC Certification Kit (for IEC 61508 and ISO 26262) 和 DO Qualification Kit (for DO-178)，可提供对行业标准的支持。
产品资源：
Polyspace 产品系列
Polyspace 产品通过在整个开发生命周期中测试和监控软件质量来保证关键代码的安全。
Polyspace Access
识别编码缺陷，查看静态分析结果，并监控软件质量指标
Polyspace Copilot
专为 Polyspace 优化的 AI 助手。
Polyspace Test
开发、管理和执行嵌入式系统中 C 和 C++ 代码的测试
Polyspace as You Code
在您的 IDE 中识别编码标准违规和软件漏洞。
Polyspace Bug Finder
运用静态分析找出软件 Bug
Polyspace Code Prover Server
持续并详尽地验证 CI 管道中的关键 C 和 C++ 代码语句。
Polyspace Bug Finder Server
通过在服务器上运行的静态分析识别软件缺陷
Polyspace Client for Ada
证明源代码中不存在运行时错误
Polyspace Code Prover
使用形式化方法详尽验证最关键的 C 和 C++ 语句。
Polyspace Server for Ada
在计算机集群上执行代码验证并发布指标
