Why3 is the next generation of the Why software verification platform. Why3 clearly separates the purely logical specification apart from generation of verification conditions for programs. It features a rich library of proof task transformations that can be chained to produce a suitable input for a large set of theorem provers, including SMT solvers, TPTP provers, as well as interactive proof assistants.
|Andrei Paskevich||François Bobot|
|...aume Melquiond||...ophe Filliatre|
|Claude Marché||Martin Clochard|