Static Analysis with Polyspace Products
Static analysis enables you to detect and prove the absence of overflow, divide-by-zero, out-of-bounds array access, and other run-time errors in source code. Polyspace® products use static code analysis and formal methods (with abstract interpretation) to verify C and C++ or Ada code. You can use Polyspace static analysis tools to verify both handwritten and generated code for embedded software.
Polyspace Bug Finder™ identifies run-time errors, data flow problems, and other defects in C and C++ embedded software. Using static analysis, Polyspace Bug Finder analyzes software control, data flow, and interprocedural behavior. It lets you triage and fix bugs early in the development process.
Polyspace Code Prover™ proves the absence of overflow, divide-by-zero, out-of-bounds array access, and certain other run-time errors in C and C++ source code. It uses formal methods-based abstract interpretation to prove code correctness. In Polyspace Code Prover run-time verification results, each operation is color-coded to indicate whether it is free of run-time errors, proven to fail, unreachable, or unproven.
Polyspace products for Ada programming language consist of the Polyspace Client™ for Ada and Polyspace Server™ for Ada. They perform static analysis to detect run-time errors and prove the absence of critical run-time errors in Ada source code.
Polyspace Bug Finder and Polyspace Code Prover help you: