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.
Papers related to Why3 verifier
- 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]