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).