http://why3.lri.fr/
Why3 is the next generation of the Why software verification platform.
Why3 clearly separates the purely logical specification part 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.
Version: 1.4.0
General Commands | |
why3 | check verification conditions in source code |
why3-cpulimit | run a command with CPU and virtual memory limits |
why3bench | schedule verification checking |
why3config | detect provers usable by why3 |
why3doc | format Why3 theories in HTML |
why3ide | start the Why3 IDE |
why3ml | generate verification conditions from Why3ML programs |
why3realize | produce a realization of a Why3 theory |
why3replayer | execute the proofs in a Why3 session file |