Polyspace^® Code Prover™ является звуковым инструментом статического анализа, который доказывает отсутствие переполнения, разделитесь на нуль, за пределы доступ к массиву и другие ошибки времени выполнения в исходном коде C++ и C. Это приводит к результатам, не требуя выполнения программы, отладки кода или тестов. Polyspace Code Prover использует семантический анализ и абстрактную интерпретацию на основе формальных методов, чтобы проверить межпроцедурное программное обеспечение, управление и поведение потока данных. Можно использовать его, чтобы проверить рукописный код, сгенерированный код или комбинацию двух. На каждый оператор кода наносят цветную маркировку, чтобы указать, свободно ли это от ошибок времени выполнения, которые, как доказывают, перестали работать, недостижимый, или бездоказательный.

Информация об области значений отображений Polyspace Code Prover для переменных и функциональных возвращаемых значений, и может доказать, какие переменные превышают указанные диапазоны. Результаты верификации кода могут использоваться, чтобы отследить метрики качества и соответствие проверки с вашими целями качества программного обеспечения. Polyspace Code Prover может использоваться с IDE Eclipse™, чтобы проверить код по вашему рабочему столу.

Поддержка промышленных стандартов доступна через IEC Certification Kit (для IEC 61508 и ISO 26262) и DO Qualification Kit (for DO-178).