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.
Polyspace Bug Finder
Kontrola dodržování pravidel kódování, bezpečnostních standardů, vyhodnocení metrik kódu a hledání chyb.
Polyspace Code Prover
Formální prokazování nepřítomnosti kritických „run-time“ chyb bez spuštění kódu.
