Produkty Polyspace provádějí statickou analýzu kódu a používají formální metody k důkazu nepřítomnosti kritických „run-time“ chyb v programu. Uvažují se všechny možné varianty průchodu kódem se všemi možnými hodnotami dat. Kontroly postihují chyby v dodržování pravidel kódování, bezpečnostní zranitelnost kódu, metriky kódu a stovky dalších skupin chyb.
Kontrola dodržování pravidel kódování, bezpečnostních standardů, vyhodnocení metrik kódu a hledání chyb.
Formální prokazování nepřítomnosti kritických „run-time“ chyb bez spuštění kódu.