Program verification with F*

Course at Summer School on Verification Technology, Systems, and Applications, VTSA 2019 at University of Luxembourg on 1-2 July 2019

Teaching team: Cătălin Hriţcu and Antoine Van Muylder

Other contributors: Danel Ahman and various other members of the F* team


Monday, 1 July 2019:

Tuesday, 2 July 2019:

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.

We also have an even cooler online editor (experimental).

For people who want to get F* (v0.9.7.0-alpha1, most recent release) installed on their machine there are 2 easy options:

  1. Using the binary release (documentation on this)
  2. or Using the OPAM package (especially for people already using OCaml; note that in this case you still need to get Z3 separately)

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

For people who are more motivated, there are even more ways, including building F* from sources (see documentation on this).

More references