Polyspace™ Embedded Software Verification
PolySpace&trade służy do weryfikacji kodu źródłowego w językach C, C++ i Ada dla aplikacji i systemów wbudowanych poprzez wykrywanie błędów wykonywnia (run-time errors) zanim kod zostanie skompilowany i wykonany. Wykorzystana technologia polega na użyciu metod formalnych aby wykryć i matematycznie udowodnić, że pewne typy błędów wykonania nie istnieją w badanym kodzie. Proponowane narzędzia mogą zostać wykorzystane zarówno dla kodu napisanego ręcznie jak i dla kodu wygenerowanego automatycznie z narzędzi do projektowania za pomocą modeli. W tym drugim przypadku PolySpace Link pozwala na śledzenie błędów bezpośrednio w modelu.