The Why3 platform

Version 0.87.3, January 2016

François Bobot1,2
Jean-Christophe Filliâtre1,2
Claude Marché2,1
Guillaume Melquiond2,1
Andrei Paskevich1,2
1 LRI, CNRS & University Paris-Sud, Orsay, F-91405
2 Inria Saclay – Île-de-France, Palaiseau, F-91120

©2010–2016 University Paris-Sud, CNRS, Inria

This work has been partly supported by the ‘U3CAT’ national ANR project (ANR-08-SEGI-021-08) ; the ‘Hi-Lite’ FUI project of the System@tic competitivity cluster ; the ‘BWare’ ANR project (ANR-12-INSE-0010) ; and the Joint Laboratory ProofInUse (ANR-13-LAB3-0007)

Part I
Tutorial

Part II
Reference Manual

Part III
Appendix

This document was translated from LATEX by HEVEA.