Polyspace Code Prover
Polyspace Code Prover™ formalnie wykazuje brak błędów przepełnienia, dzielenia przez zero, wyjścia poza rozmiar tablicy i wielu innych typowych błędów czasu wykonania w kodzie źródłowym C i C++. Narzędzie to pracuje na kodzie źródłowym, nie wymaga kompilacji, dodatkowej instrumentacji kodu czy przypadków testowych. Polyspace Code Prover wykorzystuje analizę statyczną kodu i metodę interpretacji abstrakcyjnej będącą jedną z metod formalnych analizy kodu. Może zostać wykorzystany na kodzie napisanym ręcznie jak i na kodzie wygenerowanym automatycznie lub kombinacji tych dwóch. Każda operacja w kodzie źródłowym po analizie zostanie oznaczona odpowiednim kolorem świadczącym o tym czy jest wolna od błędów, całkowicie błędna, nieosiągalna lub potencjalnie błędna.
Polyspace Code Prover udostępnia także informacje o zakresie poszczególnych zmiennych, w tym wartości zwracane przez funkcje i potrafi wykazać uwarunkowania jakie muszą zajść by wartość zmiennej wykroczyła poza zadany zakres. Wyniki pracy tego oprogramowania mogą zostać opublikowane w postaci raportu wraz z metrykami jakości kodu. Polyspace Code Prover można łatwo zintegrować z innymi narzędziami stosowanymi w procesie budowania aplikacji.
Narzędzie zapewnia wsparcie dla norm bezpieczeństwa funkcjonalnego poprzez produkty IEC Certification Kit (IEC 61508 i ISO26262) oraz DO Qualification Kit (DO-178).
