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

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

Поддержка отраслевых стандартов обеспечивается комплектом сертификации МЭК (для IEC 61508 и ISO 26262) и комплектом квалификации ДО (для DO-178).