Polyspace
制作关键代码安全可靠
Polyspace®静态代码分析产品使用形式化方法来证明一切可s manbetx 845能的控制流和数据流在缺乏关键的运行时错误。它们包括编码规则，安全漏洞，代码度量跳棋，和数百个错误的其他类的。
Polyspace代码证明器
正式证明不存在关键的运行时错误的，不执行代码
Polyspace Bug的搜索
检查编码规则，安全标准，代码度量和发现漏洞
Polyspace的阿达
证明在源代码的情况下运行时错误的
使用C / C ++和Ada正规方法自动化静态代码分析
质量
发现错误并正式证明不存在关键的运行时错误 - 没有测试用例或执行代码。
安全
符合安全标准和文件符合MISRA，ISO 26262，IEC 61508，DO-178，和FDA法规。
安全
检查软件的安全漏洞，并如CWE，CERT-C，ISO / IEC 17961，及其它标准。
日产
Polyspace认定哪些操作可以体验到运行时错误，而且能识别那些将永远不会有一个，不管工作条件。
阿莱尼亚·马基航空
Polyspace静态分析工具检查运行时错误的代码，确保符合MISRA编码标准，并为DO-178认证的信用文物。
Miracor
Polyspace帮助Miracor展示质量和正确性的监管界，包括FDA，证明我们的设备是安全的。
