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 支持开发团队和工作流。使用控制板上显示的信息来监控软件质量、项目状态、缺陷数量和代码指标。