PV2 Why3can generate correct OCaml programs or use external provers to discharge verification conditions

Why3 environment for deductive program verification is built around a kernel that implements a formal specification language, based on typed first-order logic

Application domain/field

Type of tool

Deductive verifier/verification infrastructure


Ada C Framework Java OCaml


Related papers

Last publication date


Related tools

Projects that use Why3: Frama-C, SPARK, Krakatoa

ProVerB specific

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