Polyspace Code Prover Server 是一款可靠的静态分析引擎，可以证明在 C 和 C++ 代码中不存在溢出、除以零、数组访问越界和某些其他运行时错误。它对所有可能的控制流和数据流（包括多线程代码）执行过程间分析，以将每项操作识别为始终安全、始终出错、不可达或易受攻击。Polyspace Code Prover Server 识别没有运行时错误、证明失败、不可达或未经证明的代码段。
Polyspace Code Prover Server 可以在服务器级计算机上运行，并可以使用 Jenkins® 等工具集成到编译和持续集成系统中，以进行自动验证。分析结果可以发布到 Polyspace Access 进行分类和解决。
通过 IEC Certification Kit (for ISO 26262 and IEC 61508) 和 DO Qualification Kit (for DO-178)，可提供对行业标准的支持。
使用 Polyspace Code Prover Server 自动分析代码
自动化并集成到开发运营一体化中
通过接入现有开发运营一体化工作流和工具支持现代软件开发实践。Polyspace® 可与流行的持续集成工具（如 Jenkins 和 Bamboo®）协同工作。
在任何平台上运行静态代码分析
在本地或云中的自动化服务器上运行 Polyspace Code Prover Server。使用 MathWorks 参考架构在 Docker、AWS® 和 Azure® 等平台上进行部署。
静态应用程序安全性测试
证明不存在严重的安全漏洞，例如缓冲区溢出、内存访问和数值溢出。在不执行代码的情况下使用所有代码路径和输入分析代码，从而减少对模糊测试的需求。
影响分析
正式跟踪和验证指定的全局或局部变量对其他变量或特定语句的影响。执行信号分析以满足 CARB 对 OBD 相关软件的要求，证明在满足 ISO 26262 标准的同时不受干扰，并分析标定参数的影响。在软件安全方面，执行污点分析和跟踪敏感数据流。
产品资源：
Polyspace 产品系列
Polyspace 产品通过在整个开发生命周期中测试和监控软件质量来保证关键代码的安全。
Polyspace Access
识别编码缺陷，查看静态分析结果，并监控软件质量指标
Polyspace Code Prover Server
证明软件中不存在运行时错误
Polyspace Bug Finder
运用静态分析找出软件 Bug
Polyspace Test
开发、管理和执行嵌入式系统中 C 和 C++ 代码的测试
Polyspace Bug Finder Server
通过在服务器上运行的静态分析识别软件缺陷
Polyspace Client for Ada
证明源代码中不存在运行时错误
Polyspace Code Prover
证明软件中不存在运行时错误
Polyspace Server for Ada
在计算机集群上执行代码验证并发布指标
