Polyspace Server for Ada

Perform code verification on computer clusters and publish metrics

Polyspace Server for Ada is a sound static analysis engine that proves the absence of overflow, divide-by-zero, out-of-bounds array access, and certain other run-time errors in Ada83 and Ada95 code. It performs interprocedural analysis of all possible control and data flows, including multithreaded code, to identify each operation as always safe, always faulty, unreachable, or vulnerable. Polyspace Server for Ada identifies code segments that are free of run-time errors, proven to fail, unreachable, or unproven.

You can run Polyspace Server for Ada on a server-class machine and integrate it into build and continuous integration systems for automated verification using tools such as Jenkins^®. The analysis results can be reviewed using the Polyspace Client for Ada or published to Polyspace Access for triage and resolution.

Polyspace Client for Ada uses multiple colors to identify Ada statements that have been statically checked.

Prove the Absence of Critical Run-Time Errors

Check exhaustively each Ada83 or Ada95 code operations for run-time correctness. Identify statements that will never experience a run-time error, regardless of the run-time conditions. Analyze run-time vulnerabilities with the support of event traces, variable value ranges, and call trees related to the finding. Polyspace Server for Ada uses formal methods to detect errors that elude other means of testing. Analyze all code paths against all possible inputs without code execution.

CSEE Transport Ensures Reliability of High-Speed Rail Software

Documentation

Automate and Integrate into DevOps

Supports modern software development practices by analyzing integrated code as part of existing DevOps workflows and tools. Polyspace Server for Ada works with popular continuous integration tools such as Jenkins and Bamboo^®.

Documentation

Polyspace Client for Ada provides the list of all global variables of the analyzed software.

Improve Software Design and Code Understanding

Examine control and data flow through software and see range information associated with variables and operators.

NATO HAWK Management Office Accelerates Analysis of Mission-Critical Applications

Documentation

Polyspace Client for Ada displays unreachable code in gray color within the source code.

Optimize Software for Performance

Remove defensive code by identifying safe and secure operations such as division by zero. Detect code branches that cannot be reached via any execution path and errors in logic and program structure and remove them for smaller memory footprint.

Documentation

Polyspace Client for Ada can display a graph of the path leading to potential data race.

Analyze Global Variable Usage

Reduce time spent on debugging read/write operations on global variables, including variables shared by tasks or threads Understand control and data flow leading to a data race with the concurrent access graph. Identify unused global variables for code optimization.

Documentation

Static Application Security Testing

Prove that the application is free of critical security vulnerabilities by exhaustively stressing potential vulnerable Ada statements such as memory access, buffer overflows, or numerical overflows. Support of 20 CWE weakness rules. Leverage results produced by Polyspace Server for Ada to complement or replace fuzz testing and focus instead on vulnerable operations.

Embedded Security with Polyspace Static Analysis (1:52)

Documentation

Polyspace Client for Ada computes the complete call hierarchy for Ada applications.

Improve and Complement Robustness and Functional Testing

Use Polyspace Server for Ada to improve robustness testing by focusing tests on statements proven unsafe such as division by zero or overflows. Use results from Polyspace Server for Ada to create and maintain boundary and partition tests, leveraging control and data flow analysis, and computed ranges of function parameters and global variables.

EADS Ensures Launch Vehicle Dependability

Documentation

Manage and monitor Polyspace Server for Ada projects within Polyspace Access web dashboard.

Manage Static Analysis Projects and Monitor Projects Quality

Organize your Ada static code analysis projects to support development teams and worklows with Polyspace Access. Use information displayed on the dashboards to monitor software quality, project status, number of defects, and code metrics.

Documentation

Product Resources:

Documentation Examples Videos Requirements Release notes

Interested in Polyspace Server for Ada?

Request a trial Request a quote

Have Questions?

Contact the Polyspace Server for Ada technical team.