Polyspace客户™用于阿达和Polyspace服务器™用于阿达提供代码验证，证明没有溢出的，除以零，外的界定数组访问，并且在源代码中的某些其他的运行时错误。他们使用静态代码分析不需要执行程序，代码仪器或测试用例。Polyspace产s manbetx 845品为阿达使用形式化方法技术，即抽象解释来验证码。在运行时验证结果，每个阿达操作颜色编码，以表明它是否是免费的运行时错误，证明是失败，无法访问，或未经证实的，如下：

• 绿色：免费运行时错误的证明
• 红色：每次执行操作时间证明有故障
• 灰色：证明可达（可指示功能问题）
• 橙子：未经证实的所有运行时的条件

对于阿达Polyspace服务器让您安排核查任务的计算机集群上运行。乔布斯被提交给使用Polyspace客户端阿达服务器。你可以工作整合到自动化构建流程和设置电子邮件通知。您可以通过Web浏览器查看缺陷和回归。

Polyspace为阿达帮助你：

• 检测难以发现的运行时错误和正式证明他们的缺席Ada中的源代码
• 跟踪软件质量度量并确保您的软件质量目标满足
• 视图范围信息确定的变量和函数参数和返回值的范围
• 注重与先前验证的结果相比，运行时错误差异
• 创建认证文物标准，如DO-178