The Why3 platform

Version 1.2.0, January 2019

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–2018 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), the Joint Laboratory ProofInUse (ANR-13-LAB3-0007); the ‘CoLiS’ ANR project (ANR-15-CE25-0001), and the ‘VOCaL’ ANR project (ANR-15-CE25-008).

Part I
Tutorial

Part II
Reference Manual

Part III
Appendix

This document was translated from LATEX by HEVEA.