Description: SPARK Pro is a language — a formally analyzable subset of Ada 2012 — and toolset that brings mathematics-based confidence to software verification.
AdaCore Products Overview GNAT Pro Overview Assurance Enterprise Comparison Toolsuite GNAT Dynamic Analysis Suite GNATcoverage GNATtest GNATfuzz GNAT Static Analysis Suite CodePeer GNATcheck GNATmetric SPARK Pro Overview Demos Use Cases RecordFlux Ferrocene Pricing Terms and Conditions Languages Services Overview Certification & Qualification Mentorship Training Consulting Industries Overview Domains Avionics ATM Space Rail Automotive Defense Security Medical Case Studies Standards DO-178 ESARR CAP670-SWO1
It consists of a programming language, a verification toolset and a design method which, taken together, ensure that ultra-low defect software can be deployed in application domains where high-reliability must be assured, for example where safety and security are key requirements.
SPARK 2014 offers the flexibility of configuring the language on a per-project basis - applying restrictions that allow the fine-tuning of the permitted language features as appropriate to coding standards or run-time environments.