The Spark Pro Package

AdaCore provides the SPARK Pro package as a yearly subscription which includes access to the latest versions of the technology with upgrades and Frontline support.

Toolsuite

SPARK Pro combines the renowned SPARK language and toolset from Praxis with the GPS IDE and GNAT Tracker support system from AdaCore. The toolsuite comprises the SPARK Examiner, Simplifier, Proof Checker, and other supporting tools. For details visit the SPARK Pro Language and Toolsuite page »

Frontline Support

Outstanding support is intrinsic to SPARK Pro and is supplied directly by experts and the product developers themselves from both Praxis and AdaCore. Questions on all aspects of SPARK usage and SPARK Pro are answered promptly, comprehensively, and accurately. For details visit the Frontline Support page »

The Choice For High Assurance Programming

SPARK is unique – it’s the only modern imperative programming language designed with the provision of sound static verification as the primary design goal. Through simplification of the language and the addition of contracts, SPARK also offers verification which is fast, deep, constructive and exhibits a remarkably low false-alarm rate. No other programming language or verification tools can offer this combination.

The SPARK Pro Pricing Model

The price of the yearly SPARK Pro subscription is based on the number of developers in the teams using SPARK Pro. AdaCore offers several predefined team sizes based on the maximum number of developers covered by the SPARK Pro subscription: up to 5, 15, 25, 35, 50, 100, and 200 developers overall. SPARK Pro is lock-free. All the developers covered by the subscription have constant access to the full solution: the toolset and the experts.

To request a price quote or apply for an evaluation of SPARK Pro please visit the sales information page.