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

• Deductive verification
• Verification conditions

Type of tool

Deductive verifier/verification infrastructure

Internals

• Given a WhyML program, Why3 will generate verification conditions which can be discharged using automated or interactive theorem provers.
• Users can also write WhyML programs directly and get a correct-by-construction OCaml program.
• WhyML is a language specifically for Why3. It is used as an intermediate language for the verification of C, Java, or Ada programs.