Polyspace Client™ for Ada 能够证明 Ada83 和 Ada95 源代码中不存在溢出、除以零、数组访问越界和某些其他运行时错误。它不需要执行程序、代码插桩或测试用例即可产生结果。Polyspace Client for Ada 使用基于形式化方法的抽象解释技巧来验证代码。分析结果显示在源代码中。每个代码语句都进行了着色，以指示它是否存在运行时错误、是否已证明失败、是否不可达或是否未经证明。Polyspace Client for Ada 会显示变量和函数返回值的范围信息，并且可以证明哪些变量超出了指定的范围限制。
在编译和测试之前，您可以在桌面端使用 Polyspace Client for Ada 来运行和查看代码分析。
证明不存在严重的运行时错误
检查 Ada83 或 Ada95 代码操作的运行时正确性。识别无论运行时条件如何都不会遇到运行时错误的语句。在事件跟踪、变量值范围和与发现相关的调用树的支持下，分析运行时漏洞。Polyspace Client for Ada 使用形式化方法来检测其他测试手段无法找出的错误。根据所有可能的输入，在不执行代码的情况下分析所有代码路径。
桌面端的交互式分析
组织和配置您的工程，并在将代码提交到源代码存储库之前对一部分软件工程运行静态代码分析以验证代码更改是否符合要求。使用 Polyspace Client for Ada 生成报告，并审核和对结果分类。使用类似调试器的视图步进运行时错误之前的每个语句，以找到复杂 Bug 的根本原因。
静态应用程序安全性测试
通过详尽地对潜在的易受攻击的 Ada 语句进行压力测试，如内存访问、缓冲区溢出或数值溢出，证明应用程序没有严重的安全漏洞。支持 20 条 CWE 弱点规则。利用 Polyspace Client for Ada 的分析结果来补充或取代模糊测试，转而关注易受攻击的已识别操作。
改进和补充稳健性和功能测试
使用 Polyspace Client for Ada，通过将测试重点放在已被证明不安全的语句（如除以零或溢出）上来改进稳健性测试。利用控制流和数据流分析以及计算出的函数参数和全局变量范围，使用 Polyspace Client for Ada 提供的结果来创建和维护边界测试与分区测试。
产品资源：
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
在计算机集群上执行代码验证并发布指标
