Polyspace Client for Ada
Product Description
- Introduction and Key Features
- Working with Polyspace Client for Ada
- Detect Specific Run-Time Errors in Ada Code
- Prove the Absence of Certain Run-Time Errors and Track Software Quality Metrics
- Create Artifacts for Certification
- Integrate Code Verification as Part of a Continuous Verification Process
Introduction
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 to verify code. You can use it on handwritten code, generated code, or a combination of the two, before compilation and test.
Key Features
- Verification of individual packages and package sets
- Formal methods-based abstract interpretation
- Display of run-time errors directly in code
- Eclipse™ IDE integration
Polyspace Viewer, showing color-coding for each file, procedure, and line of code.
Next
Register to view now