Polyspace Code Prover 可以证明在 C 和 C++ 源代码中不存在溢出、除以零、数组访问越界和特定的其他运行时错误。它不需要执行程序、代码插桩或测试用例即可产生结果。Polyspace Code Prover 使用基于形式化方法的静态分析和抽象解释。您可以用它来验证手写代码、生成的代码或两者的组合。每个操作都采用着色表明是否无运行时错误、证明有缺陷、不可达或未经证明。
Polyspace Code Prover 还显示变量和函数返回值的范围信息，并且可以证明哪些变量超出指定范围限制。结果可以发布到控制板上，以跟踪质量指标并确保符合软件质量目标。
通过 IEC Certification Kit (for IEC 61508 and ISO 26262) 和 DO Qualification Kit (for DO-178)，可提供对行业标准的支持。
Simulink 和 Stateflow 集成
对生成的代码运行分析，并将您的发现追溯到源 Simulink 模型模块和 Stateflow 图。从 Simulink 环境中启动 Polyspace® 分析。
产品资源：
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
证明软件中不存在运行时错误
Polyspace Bug Finder Server
通过在服务器上运行的静态分析识别软件缺陷
Polyspace Client for Ada
证明源代码中不存在运行时错误
Polyspace Code Prover
证明软件中不存在运行时错误
Polyspace Server for Ada
在计算机集群上执行代码验证并发布指标
