Polyspace examines the source code to determine where potential run-time errors such as arithmetic overflow, buffer overrun, division by zero, and others could occur.

Software developers and quality assurance managers use this information to identify which parts of the code are faulty or proven to be reliable.

Other parts of the code are marked for unproven checks and deserve individual review.

[8] It uses formal methods-based static code analysis to verify program execution at the language level.

It also produces software metrics such as Comment density of a source file, Cyclomatic complexity, Number of lines, parameters, call levels, etc.