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

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

7大方法保障嵌入式软件的安全


功能

验证 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 需要: Polyspace Bug Finder


相关解决方案

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


新闻与事件

Fast-Track MISRA Compliance of Generated Code