PV4 ⊧ SPARKchecks user-specified specifications and absence of runtime errors for Ada programsDeductive verifier for the Ada language "consists of a programming language, a verification toolset and a design method"
- Deductive verification
- Runtime verification
- Static verification
Type of toolDeductive verifier
Expected inputAda program with specifications. Specifications are written in the form of, e.g. preconditions, postconditions and loop invariants.
Format:SPARK, subset of the Ada language