PV4 ⊧ Dafnychecks user-specified annotations and languages' rules for a Dafny program

Application domain/field

• Symbolic execution
• Functional correctness
• SMT-based verifier

Type of tool

Auto-active verifier/Deductive verifier

Expected input

Program and specifications

Format:

Dafny language

Expected output

Errors if the program violates a rule of the language or if the program violates the specification.

Internals

Dafny is an SMT-based automatic program verifier. It can be used to prove functional correctness of programs. It does not require any user interaction with the solver, but the user does need to write specifications. Dafny will report errors if the program may violate a rule of the language (e.g. index bounds error) or if the program violates the specification (e.g. postcondition not established). Dafny will translate the given program (and specifications) into the verification language Boogie. Boogie will generate verification conditions based on the program, which are passed to an SMT solver (specifically Z3). Dafny is used to describe both the verifier and the language that it uses. Specifications are written in the form of preconditions, postconditions, invariants, ghost code, frame conditions, and more.

Comments

License: MIT license There is a VSCode plugin for Dafny: Repository Visual Studio Marketplace