Documentation

Polyspace Products for Ada

Prove the absence of run-time errors in source code

Polyspace® Client™ for Ada provides 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 using static code analysis that does not require program execution, code instrumentation, or test cases. Polyspace Client for Ada uses formal methods-based abstract interpretation techniques to verify code. You can use it on handwritten code, generated code, or a combination of the two, before compilation and test.

Polyspace Server™ for Ada provides 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. For faster performance, 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 e-mail notifications. You can view defects and regressions via a Web browser. You then use the client to download and visualize verification results.

Getting Started

Learn the basics of Polyspace Products for Ada

Run Verification

Detect run-time errors from Polyspace user interface, command line, or other development environments

Review Results

Investigate and fix run-time errors in verification results, organize results, results reference

Reports and Metrics

Monitor code quality through software development life cycle

Polyspace Software Administration

Software installation, activation, license configuration, client/server and web interface configuration