Polyspace Code Prover

证明软件中不存在运行时错误

Polyspace Code Prover™ 可以证明 C 和 C++ 源代码中不存在溢出、被零除、数组访问超出边界以及其他某些运行时错误。整个过程无需执行程序、植入代码,也不需要测试用例。Polyspace Code Prover 使用静态分析和基于形式化方法抽象释义。该程序可以用于手写代码、生成的代码或二者的混合。每项操作均采用颜色标记,分别表示代码无运行时错误、已证明失效、无法达到或未经证明。

Polyspace Code Prover 还会显示变量和函数返回值的范围信息,并可以证明变量是否超出指定范围限制。这些结果可以发布到控制面板上,以跟踪质量指标并确保符合软件质量目标。Polyspace Code Prover 可以集成到构建系统中以执行自动验证。

IEC Certification Kit(适用于 IEC 61508 和 ISO 26262)和 DO Qualification Kit(适用于 DO-178)提供了行业审查标准。此外,它还可以支持 Ada 语言

Comprehensive Static Analysis Using Polyspace Products

观看网上技术交流会录像

试用 Polyspace Code Prover

获取试用版软件
Jay Abraham

新增功能

来自 Jay Abraham、 Polyspace Code Prover 技术专家