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

• Deductive verification
• Language
• Runtime verification
• Static verification

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.

Format:

SPARK, subset of the Ada language

Internals

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.

Comments

License: GPL v3.0