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

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 语言


功能

验证 C 和 C++ 嵌入式软件

执行 C 和 C++ 嵌入式软件的代码验证,该验证必须按照最高质量和安全等级进行。

了解更多

检测运行时错误

证实、发现和诊断溢出、被零除和指针越界等运行时错误。

了解更多

查看范围信息

跟踪通过软件的控制流和数据流,并显示与变量和运算符相关的范围信息。

了解更多

跟踪软件质量指标

定义一个集中式质量模型来跟踪运行时错误、代码复杂度以及编码违规。

了解更多

依据代码验证结果回溯至 Simulink 模型

验证生成的代码或混合代码(同时包含自动生成代码和手写代码)。

了解更多

实现代码验证流程自动化

自动调度验证作业并设置电子邮件通知。

了解更多

创建认证工件

根据行业标准完成项目认证流程。

了解更多

产品资源

通过浏览这些资源,探索有关 Polyspace Code Prover 的更多信息。

文档

浏览 Polyspace Code Prover 函数和功能文档,包括发行说明和代码示例

系统要求

查看最新 Polyspace Code Prover 版本的系统要求

技术文章

查看使用 Polyspace Code Prover 方面的文章,了解可以带来的技术优势

用户案例

了解 Polyspace Code Prover 正在如何推动您所在行业内的研发步伐

社区和支持

查找问题答案并浏览故障排除资源

应用程序

Polyspace Code Prover 应用程序可让您通过一个交互式界面快速执行常见任务


试用或购买

开始使用Polyspace Code Prover 产品有多种方式。 下载免费试用版, or 了解定价和许可选项。

获取免费试用版

试用 Polyspace Code Prover。

获取试用版

准备购买?

购买 Polyspace Code Prover 并了解附加产品。

联系销售
定价和许可

有疑问吗?

Ram

联系 Ram Cherukuri,
Polyspace Code Prover 技术专家

给 Ram 发送电子邮件

Polyspace Code Prover requires Polyspace Bug Finder.


相关解决方案

使用 Polyspace Code Prover 来解决科技与工程上的挑战:


新闻与事件

Fast-Track MISRA Compliance of Generated Code