PV4 SPARKchecks user-specified specifications and absence of runtime errors for Ada programs

Deductive verifier for the Ada language "consists of a programming language, a verification toolset and a design method"

Application domain/field

Type of tool

Deductive verifier

Expected input

Ada program with specifications. Specifications are written in the form of, e.g. preconditions, postconditions and loop invariants.


SPARK, subset of the Ada language


The functional specification features in SPARK are executable. So the verification can be done dynamically or statically. The name SPARK is used for the verifier, but also for the language, which is a subset of Ada. SPARK uses GNATprove for the verification. SPARK uses Why3 to generate verification conditions. It uses Alt-Ergo, CVC4 and/or Z3 to discharge the verification conditions.


License: GPL v3.0


Related papers

Last publication date

19 December 2020

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.