PV4 ⊧ Boogieinfers invariants and generates verification conditions to pass to Z3

Application domain/field

Static program verification

Type of tool

Verification framework

Expected input

Program

Format:

Boogie language (.bpl file)

Expected output

Error message for any assertions, preconditions, postconditions, or loop invariants that could not be proven correct.

Internals

The verifier, given a Boogie program, generates verification conditions (VCs) that are passed to an SMT solver. Uses Z3, CVC4, Yices

Comments

Intermediate verification language & verifier It is intended as a layer to build program verifiers on top of. License: MIT