Why3 verifier

[Google Scholar] [Website]

Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions.

todo:

Frama-C: A software analysis perspective [cuoq:sefm:2012]
The Why/Krakatoa/Caduceus platform for deductive program verification [filliatre:cav:2007]
Why3 — where programs meet provers [filliatre:esop:2013]
Multi-prover verification of C programs [filliatre:fem:2004]

The opinions expressed are my own views and not my employer’s.