Polyspace Products for Ada
Prove the absence of run-time errors in source code
Polyspace Client™ for Ada and Polyspace Server™ for Ada provide code verification that proves the absence of overflow, divide-by-zero, out-of-bounds array access, and certain other run-time errors in source code. They use static code analysis that does not require program execution, code instrumentation, or test cases. Polyspace products for Ada use a formal methods technique called abstract interpretation to verify code. In the run-time verification results, each Ada operation is color-coded to indicate whether it is free of run-time errors, proven to fail, unreachable, or unproven, as follows:
Polyspace Server for Ada lets you schedule verification tasks to run on a computer cluster. Jobs are submitted to the server using Polyspace Client for Ada. You can integrate jobs into automated build processes and set up email notifications. You can view defects and regressions via a Web browser.
Polyspace for Ada helps you: