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

Schedule

Monday, 7 May, 2018:

15:15--16:45 Cătălin: A Gentle Introduction to F*: Verifying purely functional programs (code)

Tuesday, 8 May, 2018:

10:45--12:15 Cătălin: Verifying Stateful Programs with F* (code)
13:45--15:00 Danel: Monotonic State in F* (code)
15:30--16:30 Cătălin: F*'s effects, tactics, WPs, and SMT encoding
16:45--18:00 Antoine: Security verification and cryptographic modelling in F*

Code and exercises from slides

https://github.com/catalin-hritcu/fstar-course-epit2018

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:

Using the latest binary release (v0.9.6.0-alpha1) (documentation on this)
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 INSTALL.md.

More references