Polyspace Code Prover Server
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 Server™ może działać na maszynie klasy serwerowej i może być zintegrowany z systemami do tworzenia i ciągłej integracji, w celu zautomatyzowanej weryfikacji przy użyciu narzędzi takich jak Jenkins. Wyniki analizy można opublikować w programie Polyspace Code Prover Access™
w celu dalszej oceny i analizy.
