Polyspace Code Prover Server 可集成到持续集成流水线中,用于证明 C/C++ 代码中不存在某些运行时错误,例如溢出、除以零以及数组越界访问。它还提供有关控制流和数据流的洞察,并验证跨任务(线程)对共享内存的并发访问是否正确。
Polyspace Code Prover Server 使用基于抽象解释和形式化方法的静态分析,无需执行代码、添加插桩或编写测试用例即可提供结果。您可以将结果上传到 Polyspace Access,以便进行协作和质量趋势跟踪,并可导出为适合 CI 质量门的机器可读格式。您可以分析任何组合的 C/C++ 代码,无论是手动编写的,还是由 Simulink 或 AI 助手生成的。
通过 IEC Certification Kit (for ISO 26262 and IEC 61508) 和 DO Qualification Kit (for DO-178),可提供对行业标准的支持。
自动化并集成到开发运营一体化中
通过接入现有开发运营一体化工作流和工具支持现代软件开发实践。Polyspace® 可与流行的持续集成工具(如 Jenkins 和 Bamboo®)协同工作。
在任何平台上运行静态代码分析
在本地或云中的自动化服务器上运行 Polyspace Code Prover Server。使用 MathWorks 参考架构在 Docker、AWS® 和 Azure® 等平台上进行部署。
产品资源:
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
在计算机集群上执行代码验证并发布指标