Polyspace Server for Ada 是一个可靠的静态分析引擎，可以证明在 Ada83 和 Ada95 代码中不存在溢出、除以零、数组访问越界和某些其他运行时错误。它对所有可能的控制流和数据流（包括多线程代码）执行过程间分析，以将每项操作识别为始终安全、始终出错、不可达或易受攻击。Polyspace Server for Ada 可识别没有运行时错误、已证明失败、不可达或未经证明的代码段。
您可以在服务器级别计算机上运行 Polyspace Server for Ada，并使用 Jenkins® 等工具将其集成到编译和持续集成系统中进行自动验证。分析结果可使用 Polyspace Client for Ada 进行审核，或发布到 Polyspace Access 进行分类和解决。
证明不存在严重的运行时错误
详尽检查每个 Ada83 或 Ada95 代码操作的运行时正确性。识别无论运行时条件如何都永远不会遇到运行时错误的语句。在事件跟踪、变量值范围和与发现相关的调用树的支持下，分析运行时漏洞。Polyspace Server for Ada 使用形式化方法来检测其他测试手段无法找出的错误。在不执行代码的情况下，针对所有可能的输入分析全部代码路径。
自动化并集成到开发运营一体化中
将分析集成的代码作为现有开发运营一体化工作流和工具的一部分，以此支持现代软件开发实践。Polyspace Server for Ada 可与流行的持续集成工具（如 Jenkins 和 Bamboo®）协同工作。
静态应用程序安全性测试
通过详尽地对潜在的易受攻击的 Ada 语句进行压力测试，如内存访问、缓冲区溢出或数值溢出，证明应用程序没有严重的安全漏洞。对 20 条 CWE 弱点规则的支持。利用 Polyspace Server for Ada 生成的结果来补充或取代模糊测试，转而关注易受攻击的操作。
改进和补充稳健性和功能测试
使用 Polyspace Server for Ada，通过将测试重点放在证明不安全的语句（如除以零或溢出）上来改进稳健性测试。利用控制流和数据流分析以及计算出的函数参数和全局变量范围，使用 Polyspace Server for Ada 提供的结果来创建和维护边界测试与分区测试。
管理静态分析项目并监控项目质量
组织您的 Ada 静态代码分析项目，以使用 Polyspace Access 支持开发团队和工作流。使用控制板上显示的信息来监控软件质量、项目状态、缺陷数量和代码指标。
产品资源：
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
在计算机集群上执行代码验证并发布指标
