SPARK Pro Product Update
SPARK Pro is a language and toolset that allows developers to formally define and automatically verify software requirements to guarantee that a program behaves as intended. You can adopt SPARK either at the beginning of a project, or by progressively integrating it in an existing codebase developed, for example, in Ada, C or C++.
AdaCore’s release of SPARK Pro 21.0 expands its support of Ada language constructs, allowing more programs to be effectively specified and verified, and provides better tool interactions with improved tool messages and guidance.
Check out this video to discover how the latest capabilities in SPARK 21.0 can help you save time and effort while reaping the full benefits of formal program verification.
