Gentle Introduction to Formal Methods

Get Started

If you are interested in running and experimenting with the code examples, please visit:
http://why3.lri.fr/ for general information and https://www.lri.fr/~marche/MPRI-2-36-1/install.html to install the tools needed under Ubuntu using the opam package manager.

First-Order Logic

If you are not familiar with the notion of first-order logic, no worries, you will get it. You may see it as an extension to propositional logic, including functions over values. You may check wikipedia https://en.wikipedia.org/wiki/First-order_logic for an overview, but it is quite hard-core. In the below you will find some examples that help you understand.

Contract Based Verification, and Hoare-logic

To be completed.

The Why3 platform and the WhyML language

To be completed.

Why3 and SMT Solvers

To be completed.

/Per Lindgren, September 2015