Program verification with F*

Course at EPIT 2018 Software Verification Spring School in Aussois, France on 7-8 May, 2018

Teaching team: Cătălin Hriţcu, Antoine Delignat-Lavaud, Danel Ahman, and Victor Dumitrescu


Monday, 7 May, 2018: Tuesday, 8 May, 2018:

Code and exercises from slides

Setup instructions

The easiest way to try out F* quickly is directly in your browser using the online editor that's part of the F* tutorial.
And now we also have an even cooler online editor (very experimental, module name needs to be called STLC).

For people who want to get F* (v0.9.6.0-alpha1 released on Friday) installed on their machine there are 2 easy options:

  1. Using the latest binary release (v0.9.6.0-alpha1) (documentation on this)
  2. or Using the OPAM package (especially for people already using OCaml)

In addition, if you're familiar with emacs we recommend getting fstar-mode.

For people who are more motivated, there are even more ways including building things from sources.
It's all documented in

More references